© 2022 Steven Obua

Automating Abstraction Logic

by Steven Obua
Cite as: https://doi.org/10.47757/aal.1
March 23rd, 2022
We describe how to automate Abstraction Logic by translating it to the TPTP THF format.


It is clear that interweaving user instructions with sophisticated artificial intelligence is the future of interactive theorem proving. A particularly successful version of this has been pioneered by Sledgehammer [1]. Its basic idea is to interface the Isabelle [2] proof assistant with external automated reasoning systems like E prover [3] which support problem specifications in one of the TPTP formats. These formats include FOF for classical first-order logic, and THF for classical higher-order logic.
Can we do something similar for Practal and Abstraction Logic [4] (AL)? A first quick experiment, which we describe in the following, confirms that yes, we can.

The Experiment

The experiment consists of translating the inference rules of AL and the first ten axioms listed in Abstraction Logic [4] to THF, and proving the principle of explosion from them using E prover. This translation to THF can be done automatically for any set of AL terms, and it is therefore enough to concentrate here on a simple example of just ten axioms.
It might be surprising that we can actually do such a translation from AL to THF. After all, AL is a very general logic (actually, we have argued before that it is the most general logic) and includes intuitionistic logic, but THF problems are described in classical logic. In particular, our ten axioms describe a logic even weaker than intuitionistic logic, so how can a classical proof yield (the existence of) an even-weaker-than-intuitionistic-logic proof?
This is possible because we will actually be describing in THF the models of the AL axioms. These models are abstraction algebras, and can be described easily using classical logic and THF. Because AL is complete for our ten axioms (and any other set of axioms which include at least the first eight axioms), proving a property for all models (using classical logic or whatever other method) is equivalent to the existence of a proof of the corresponding theorem in AL.


We introduce the following THF constants to describe our models:
thf(const_true, type, (true : $i)).
thf(const_implies, type, (implies : $i > ($i > $i))).
thf(const_forall, type, (forall : ($i > $i) > $i)).
thf(const_eq, type, (eq: $i > ($i > $i))).
thf(const_false, type, (false : $i)).
thf(const_not, type, (not : ($i > $i))).
Here true corresponds to \top and is an element of the abstraction algebra. The universe U\mathcal{U} of our abstraction algebra is described in THF by $i, the type of individuals. Another element of U\mathcal{U} is false, which models \bot. Negation ¬¬ is modelled by the THF constant not. Negation is a unary operation, and thus not has type $i > $i, where > is used in THF to denote the type of functions. Implication and equality == are binary operations, and represented in THF by the constants implies and eq, both having type $i > ($i > $i). Finally, we represent universal quantification \forall, which is a proper unary operator, by the THF constant forall of type ($i > $i) > $i.

Inference Rules

Abstraction Logic has four proof rules:
The first two rules do not describe any properties of abstraction algebras. They have corresponding counterparts already integrated in THF, and do not need to be encoded explicitly. This leaves us with the two inference rules modus ponens and introduction of universal quantification. We state modus ponens in THF as follows:
thf(modusPonens, axiom, (! [U : $i]: 
  (((implies @ true @ U) = true) => (U = true)))).
Introduction of universal quantification looks in THF like this:
thf(allIntro, axiom, (! [F : ($i > $i)]: 
  ((! [U : $i]: ((F @ U) = true)) => ((forall @ F) = true)))).
The THF symbols !, => and = represent universal quantification, implication and equality of classical logic, respectively. Note that these are distinct from the AL operators forall, implies and eq, which represent operators of an abstraction algebra. Function application @ means the same in THF as in the semantics of AL operators.
These two THF axioms are direct translations of the defining properties of logic algebras in Abstraction Logic [4]:
From here the THF axioms follow by realising that I()=I(\top) = {\includegraphics[height=0.5em]{0297DAFD-A9C8-4D30-B899-0842E1F3F710}}, I()=I(⇒) = {\includegraphics[height=0.5em]{89B2C8A0-68B9-4536-B3AF-413BC50BE6DF}} and I()=I(\forall) = {\includegraphics[height=0.5em]{2BEC3123-1D57-4034-91CF-15740353FD77}}.


The first ten axioms from Abstraction Logic [4] are:
  1. A(BA)A ⇒ (B ⇒ A)
  2. (A(BC))((AB)(AC))(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))
  3. (x.A[x])A[x](∀ x.\,A[x]) ⇒ A[x]
  4. (x.AB[x])(A(x.B[x]))(∀ x.\,A ⇒ B[x]) ⇒ (A ⇒ (∀ x.\, B[x]))
  5. x=xx = x
  6. x=y(A[x]A[y])x = y ⇒ (A[x] ⇒ A[y])
  7. A(A=)A ⇒ (A = ⊤)
  8. =(x.x)⊥ = (∀ x.\, x)
  9. ¬A=(A)¬ A = (A ⇒ ⊥)
Translating these axioms to THF is straightforward:
Axiom 1 translates to true = true, and can therefore be omitted. For the remaining nine axioms we obtain the following translations to THF:
thf(ax2, axiom, (! [A : $i, B : $i]: ((implies @ A @ (implies @ B @ A)) = true))).
thf(ax3, axiom, (! [A : $i, B : $i, C : $i]: 
    @ (implies @ A @ (implies @ B @ C)) 
    @ (implies @ (implies @ A @ B) @ (implies @ A @ C)))
  = true))).
thf(ax4, axiom, (! [X : $i, A : ($i > $i)]: 
    @ (forall @ A) 
    @ (A @ X)) = true))).
thf(ax5, axiom, (! [A : $i, B : ($i > $i)]: 
    @ (forall @ (^[X : $i]: (implies @ A @ (B @ X))))
    @ (implies @ A @ (forall @ B))) = true))).
thf(ax6, axiom, (! [X : $i]: ((eq @ X @ X) = true))).
thf(ax7, axiom, (! [X : $i, Y : $i, A : ($i > $i)]: 
    @ (eq @ X @ Y)
    @ (implies @ (A @ X) @ (A @ Y))) = true))).
thf(ax8, axiom, (! [A : $i]: ((implies @ A @ (eq @ A @ true)) = true))).
thf(ax9, axiom, ((eq @ false @ (forall @ (^[X : $i]: X))) = true)).
thf(ax10, axiom, (![A : $i]: 
    @ (not @ A)
    @ (implies @ A @ false)) = true))).

Proving with E

The principle of explosion states that from AA and ¬A¬ A we can deduce anything: A((¬A)B)A ⇒ ((¬ A) ⇒ B) Translating this to THF results in the following conjecture:
thf(explosion, conjecture, (! [A : $i, B : $i]: 
   @ A
   @ (implies @ (not @ A) @ B)) = true))).
The complete THF text file explosion.txt which integrates constants, inference rules, axioms and conjecture is available.
Running [3] on this file can be done via
eprover-ho -s explosion.txt --auto-schedule
and yields the satisfying message Proof found!.
The above translation from AL to THF has been performed manually. It is easily possible to automate this process. Without further simplification, this yields slightly more complicated THF output, which can be inspected here. The difference is big enough to cause E to fail on this automatically generated THF file. Petar Vukmirović told me that he just completed a version of E which includes many of the improvements from his paper on higher-order superposition [5]. It is available under the wip-bce branch of E prover. As it turns out, this version of E can solve the generated THF file without problems!


We have illustrated how to translate Abstraction Logic to THF. This makes it possible to apply existing automated reasoning systems like E to Abstraction Logic. To confidently accept E’s proof of a translated theorem as a derived inference rule for Abstraction Logic, we need to make sure that E’s semantic for THF, Henkin semantics, actually covers all AL models. This seems plausible and likely, but a careful proof of this is desirable. Another possibility is to use E’s capability of producing proof objects to infer an AL proof of the theorem. If we succeed in doing so, in principle we can skip explaining the connection between THF’s Henkin semantics, and AL semantics. More importantly, this has also the advantage that we do not need to trust the correctness of E’s implementation.
Although a translation of AL to THF is possible, it is clear that THF is a more complicated logic than AL. For example, matching of AL terms is decidable, while it is not known to be decidable for general THF terms. In light of this, developing automated reasoning algorithms specifically for Abstraction Logic could be fruitful.


[1]Laurence C. Paulson, Jasmin Blanchette. (2012). Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers, https://doi.org/10.29007/36dt.
[2]Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. (2019). From LCF to Isabelle/HOL, https://doi.org/10.1007/s00165-019-00492-1.
[3]Stephan Schulz, Simon Cruanes, Petar Vukmirović. (2019). Faster, Higher, Stronger: E 2.3, https://doi.org/10.1007/978-3-030-29436-6_29.
[4]Steven Obua. (2021). Philosophy of Abstraction Logic, https://doi.org/10.47757/pal.2.
[5]Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, Sophie Tourret. (2022). Making Higher-Order Superposition Work, https://doi.org/10.1007/s10817-021-09613-z.