Automating Abstraction Logic
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 artiﬁcial intelligence is the future of interactive theorem proving. A particularly successful version of this has been pioneered by Sledgehammer 
. Its basic idea is to interface the Isabelle 
proof assistant with external automated reasoning systems like E prover 
which support problem speciﬁcations in one of the TPTP
formats. These formats include FOF
for classical ﬁrst-order logic, and THF
for classical higher-order logic.
Can we do something similar for Practal
and Abstraction Logic 
(AL)? A ﬁrst quick experiment, which we describe in the following, conﬁrms that yes, we can.
The experiment consists of translating the inference rules of AL and the ﬁrst ten axioms listed in Abstraction Logic 
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 ﬁrst 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))).
and is an element of the abstraction algebra. The universe
of our abstraction algebra is described in THF by $i
, the type of individuals. Another element of
, which models
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
are binary operations, and represented in THF by the constants implies
, both having type $i > ($i > $i)
. Finally, we represent universal quantiﬁcation
, which is a proper unary operator, by the THF constant forall
of type ($i > $i) > $i
- axiom invocation
- modus ponens
- introduction of universal quantiﬁcation
The ﬁrst 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 quantiﬁcation. We state modus ponens in THF as follows:
thf(modusPonens, axiom, (! [U : $i]:
(((implies @ true @ U) = true) => (U = true)))).
Introduction of universal quantiﬁcation 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 quantiﬁcation, 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 deﬁning properties of logic algebras
in Abstraction Logic 
- implies for all values in .
- Let be any unary operation of such that for all values in . Then .
From here the THF axioms follow by realising that
Translating these axioms to THF is straightforward:
- There is an obvious and simple strategy for translating any AL term to a THF term.
- To express that the AL term is actually an axiom, we then equate the translated term to true.
- Finally, we universally quantify over all free variables.
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)))
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
we can deduce anything:
Translating this to THF results in the following conjecture:
thf(explosion, conjecture, (! [A : $i, B : $i]:
@ (implies @ (not @ A) @ B)) = true))).
The complete THF text ﬁle explosion.txt
which integrates constants, inference rules, axioms and conjecture is available
Running E 
on this ﬁle 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 simpliﬁcation, 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 ﬁle. 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 
. It is available under the wip-bce
branch of E prover. As it turns out, this version of E can solve the generated THF ﬁle 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 conﬁdently 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 speciﬁcally for Abstraction Logic could be fruitful.
(2012). Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers, https://doi.org/10.29007/36dt.