Automating Abstraction Logic

March 23rd, 2022

Abstract

We describe how to automate Abstraction Logic by translating it to the TPTP THF format.

Introduction

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 [1]. Its basic idea is to interface the Isabelle [2] proof assistant with external automated reasoning systems like E prover [3] 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 [4] (AL)? A ﬁrst quick experiment, which we describe in the following, conﬁrms that yes, we can.

The Experiment

The experiment consists of translating the inference rules of AL and the ﬁrst 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 ﬁ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.

Constants

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

\mathcal{U}

of our abstraction algebra is described in THF by $i, the type of individuals. Another element of

\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 quantiﬁcation

\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:

axiom invocation
substitution
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 [4]:

$I(⇒)(I(\top), u) = I(\top)$ implies $u = I(\top)$ for all values $u$ in $\mathcal{U}$ .
Let $f$ be any unary operation of $\mathcal{U}$ such that $f(u) = I(\top)$ for all values $u$ in $\mathcal{U}$ . Then $I(\forall)(f) = I(\top)$ .

From here the THF axioms follow by realising that

I(\top) = {\includegraphics[height=0.5em]{0297DAFD-A9C8-4D30-B899-0842E1F3F710}}

I(⇒) = {\includegraphics[height=0.5em]{89B2C8A0-68B9-4536-B3AF-413BC50BE6DF}}

and

I(\forall) = {\includegraphics[height=0.5em]{2BEC3123-1D57-4034-91CF-15740353FD77}}

Axioms

The ﬁrst ten axioms from Abstraction Logic [4] are:

$⊤$
$A ⇒ (B ⇒ A)$
$(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))$
$(∀ x.\,A[x]) ⇒ A[x]$
$(∀ x.\,A ⇒ B[x]) ⇒ (A ⇒ (∀ x.\, B[x]))$
$x = x$
$x = y ⇒ (A[x] ⇒ A[y])$
$A ⇒ (A = ⊤)$
$⊥ = (∀ x.\, x)$
$¬ A = (A ⇒ ⊥)$

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  
    @ (implies @ A @ (implies @ B @ C)) 
    @ (implies @ (implies @ A @ B) @ (implies @ A @ C)))
  = true))).
thf(ax4, axiom, (! [X : $i, A : ($i > $i)]: 
  ((implies 
    @ (forall @ A) 
    @ (A @ X)) = true))).
thf(ax5, axiom, (! [A : $i, B : ($i > $i)]: 
  ((implies 
    @ (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)]: 
  ((implies 
    @ (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]: 
  ((eq 
    @ (not @ A)
    @ (implies @ A @ false)) = true))).

Proving with E

The principle of explosion states that from

A

and

¬ A

we can deduce anything:

A ⇒ ((¬ A) ⇒ B)

Translating this to THF results in the following conjecture:

thf(explosion, conjecture, (! [A : $i, B : $i]: 
 ((implies 
   @ A
   @ (implies @ (not @ A) @ B)) = true))).

The complete THF text ﬁle explosion.txt which integrates constants, inference rules, axioms and conjecture is available.

Running E [3] 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 [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 ﬁle without problems!

Conclusion

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.

References

[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.