2.1 Roy Dyckhoff’s G4ip calculus

Motivated by problems related to loop avoidance in implementing Gentzen’s LJ calculus, Roy Dyckhoff designed and proved sound and complete a sequent calculus-based axiomatization of IL (Dyckhoff Reference Dyckhoff1992). He has proved that the calculus is terminating, by identifying a multiset ordering-based formula size definition that decreases after each step (Dyckhoff Reference Dyckhoff1992).

The sequents of the G4ip calculus follow:

Key to the termination proof in Dyckhoff (Reference Dyckhoff1992) is the rule $L\!\rightarrow\!\rightarrow$ that breaks down nested implications into “smaller” ones, each containing fewer connectives. The rules work with the context $\Gamma$ being a multiset, but it has been shown later (Dyckhoff Reference Dyckhoff2016) that $\Gamma$ can be a set, with duplication in contexts eliminated.

Note that the same calculus has been discovered independently in the 1950s by Vorob’ev and in the 1980s-1990s by Hudelmaier (Reference Hudelmaier1988).

2.2 Implementing the theorem prover

In the tradition of “lean theorem provers”, we can build one directly from the G4ip calculus, in a goal oriented style, by reading the rules from conclusions to premises.

Thus, we start with a simple, almost literal translation of sequent rules to Prolog with values in the environment $\Gamma$ denoted by the variable Vs. Besides implication (denoted ->), conjunction (denoted &) and disjunction (denoted v), we implement rules for inverse implication (denoted ), negation (denoted | |) and equivalence (denoted ). We also add rules for a top element (denoted true) and a bottom element (denoted false).

Correctness of our additions follows from the definitions of:

• intuitionistic inverse implication: $\varphi \leftarrow \psi ~\equiv~ \psi \rightarrow \varphi$

• intuitionistic equivalence: $\varphi \leftrightarrow \psi \equiv \varphi \rightarrow \psi ~ \verb~&~ ~ \psi \rightarrow \varphi$

• intuitionistic negation: $ \verb|~|\varphi ~\equiv~ \varphi \rightarrow \verb~false~$ .

• top element: $\verb~true~ ~\equiv~ \verb~false~ \rightarrow \verb~false~ $ .

Note that the added connectives are meant to enhance the expressiveness of the logic. For instance, “” allows expressing the fact that two formulas are equivalent and thus equiprovable, “head body” mimics Prolog’s familiar Horn clause syntax “ head :- body” and finally the negation symbol makes formulas more compact and human-readable.

We define operators for all our connectives, except ->, that we will use with its standard right associativity.

A formula T is a theorem if it is provable from an empty set of assumptions:

We follow here Dyckhoff’s calculus but delegate details to helper predicates iprover_reduce/4 and iprover_impl/4.

iprover_reduce/4 is the first step in breaking down formulas in the premise into their components.

iprover_impl/4 details the case analysis of the handling of implication (and its instances) prescribed by rule $L\!\rightarrow\!\rightarrow$ .

we observe success on proving a tautology and failing to prove a contradiction, but we refer to Tarau (Reference Tarau2019) for an extensive combinatorial testing of a variant of this prover as well as its testing against the ILTP benchmark ^{Footnote 3} and several other provers.

2.3 Classical logic for free

Glivenko’s theorem states that a propositional formula F is a classical tautology if and only if $\tilde ~~ \tilde ~ F$ is an intuitionistic tautology. This gives us a classical prover for free, that we will use as an alternative to iprove when defining several concepts parameterized by a prover.

but agree on |p & p|:

3.1 Generating the abducibles

Defining some of the atoms occurring in a formula F as the only ones to be used in the search process brings us to declare them as abducibles (Eshghi and Kowalski Reference Eshghi and Kowalski1989), but we will also enable the option to make abducible all the atoms occurring in F. Thus, when the variable Abducibles is free, all atomic symbols will be considered abducibles.

The predicate atoms_of/2 finds the set of all the atoms occurring in a formula. It backtracks over all arguments, recursively and it collects atomic elements to a list, with setof/3 which also eliminates possible duplicates.

3.2 Protasis generation

If F is a formula, we can think of a premise C such that $C \rightarrow F$ is a theorem ^{Footnote 4} as a counterfactual assumption making F conditionally true. We call such a formula C a protasis. Thus, given a formula and a set of assumptions (our abducibles), we will need to search among them for assumptions that would make the formula a theorem.

The predicate any_protasis/6 implements this idea, subject to a set of parameters:

• Prover allows a choice of the underlying logic (e.g., intuitionistic or classical)

• AggregatorOp fixes one of the connectives of the logic, from which the protasis is built ^{Footnote 5}

• The yes/no flag WithNeg decides if negations of the abducibles can be part of the protasis

• Abducibles is a set of atoms or a free variable, meaning that all atoms will be included

• Assumption will be any protasis, that given the previously specified parameters, ensures that Assumption->Formula is a theorem in the logic specified by Prover.

The predicate mark_hypos/3 will mark with their negations the abducibles if we want to allow them to occur in the protasis positively or prefixed by their negations.

Our subset generator subset_of, used to iterate over all subsets of the abducibles, first enumerates templates of increasing length as we want smaller subsets to be tried first.

Then, for each template of length K, it fills it with a subset of length K of the N abducibles, one at a time, on backtracking.

The predicate join_with_op builds an expression from a sequence of abducible literals (atoms, possibly negated) with a given operator.

How we join the abducible literals with help of a given operator, is different for associative and commutative operators like & and v (the default 3-rd clause of join_with) and ->, , , that we treat as special cases.

Thus, once the head was picked with select/3, the order of the remaining literals is immaterial.

For non-associative we will use all permutations of the abducibles.

Finally, as v and & are permutation invariant, we just call join_with_op.

Implication and reverse implications are handled in join_with, knowing that their components, except the head, are permutation invariant, with the following equivalences in mind:

\begin{align*}\varphi_0 \leftarrow \varphi_1 \dots \leftarrow \varphi_n \equiv \varphi_0 \leftarrow \varphi_1 ~\&~ \dots ~\&~ \varphi_n\end{align*}

and

\begin{align*}\varphi_n \rightarrow \varphi_{n-1} \dots \rightarrow \varphi_1 \rightarrow \varphi_0 ~\equiv~ \varphi_n ~\&~ \varphi_{n-1} ~\&~ \dots ~\&~ \varphi_1 ~\rightarrow \varphi_0\end{align*}

Note that these hold both intuitionistically and classically, as it can be quickly verified with iprover and cprover.

3.3 The weakest protasis

The next step is defining a weakest protasis, keeping in mind that a partial order ^{Footnote 6} among them is defined by the intuitionistic implication (->). First, we will collect with setof/3 all the candidate assumptions to ensure that the prover is called on each only once.

Next, we ensure that a weakest protasis is such that it does not imply any other protasis, thus that it is a minimal element w.r.t. our partial order. We rely for that on the predicate weakest_with/3:

The partial order relation is exposed as the predicate weaker_with/3 which ensures that a weakest protasis does not imply any other protasis, including ones that might imply it.

Note that the predicate weakest_protasis/6 depends on the same parameters as any_protasis, in particular on the Prover implementing a given provability relation.

When running it we get:

This reveals an interesting fact. It tells us that if |p v p| were assumed, Peirce’s law would hold in IL, as iprove would succeed. As it is well known, |p v p| would turn IL into CL and cprove tells us that indeed, Peirce’s law holds unconditionally in CL.

we obtain:

showing that the implication d->c (equivalent of the Horn Clause c:-d) should hold for the formula to be a theorem. This illustrates a mechanism to synthesize Horn Clauses playing the role of conditional assumptions.

Another interesting case is that of a contradiction. After defining contra_test/1 as:

and running it with:

we can see that no assumption would make the contradiction a tautology, and this will also be the case for Prover=cprover. Note that to ensure this, we have enforced in the definition of any_protasis that such assumptions should themselves not be contradictions.

| f v (f->g) v g|

as shown in Lifschitz et al. (Reference Lifschitz, Pearce and Valverde2001), we will get with cprover the protasis true. This indicates, as expected, that it is already a theorem in CL and thus also a theorem in the logic of here-and-there.

On the other hand, the less obvious weakest protasis obtained for iprove indicates that the excluded middle rule would be needed for both f and g.

3.4 An example of intuitionistic abductive reasoning

With the logic of synthesizing meaningful minimal assumptions that make a formula a theorem clarified, we are now ready to revisit abductive reasoning along the lines of Eshghi and Kowalski (Reference Eshghi and Kowalski1989). The predicate explain_with/5 finds, given a Prover, the abductive inference problem parameterized by:

• a formula Prog seen here as representing a knowledge base

• a set of Abducibles occurring in Prog

• a goal formula G such that Prog -> G should always hold

• a formula IC playing the role of integrity constraints meant to filter out unwanted assumptions

Note also that any_protasis replaces weakest_protasis in this definition, given that minimality might want to be stated as part of the integrity constraints IC.

Then, when running it, it will display, as expected:

4.1 The Mints transformation

Grigori Mints has proven, in his seminal paper studying complexity classes for intuitionistic propositional logic (Mints Reference Mints1992), that any formula f is equiprovable to a formula of the form $X_f \rightarrow g$ , where $X_f$ is a conjunction of formulas of one of the forms:

$$p,\verb|~|p, \, p \to q,(p \to q) \to r,p \to (q \to r),p \to (q ~v~ r),p \to \verb|~|q, \, \verb|~|q \to p.$$

With introduction of new variables (like with the Tseitin transform for SAT or ASP solvers), the transformation runs in linear space and time. Note that as a premise to a sequent can be seen as a conjunction implying its conclusion, the conjunction of the formulas described by Mints can be seen as serving the same purpose as the conjunctive normal form (CNF) in classical logic.

Thus, by generating this set of bounded size formulas as premises of a sequent, we can express equivalent formulas of unbounded size, otherwise subject to a much larger search space in the formula synthesis process.

We will now generate, using a given set of abducibles, premises built of these formulas, with their propositional variables selected from the set of abducibles.

Conceptually, while we will keep calling the propositional variables involved in our premise abducibles, we shall see them from now on simply as a set of independent variables on which the derivation of the sequent’s conclusion from its premise depends.

We define a generator for the set of Mints formulas with help of a DCG grammar ^{Footnote 7} that collects its propositional variables from a list of abducibles.

We extend our DCG, subject to the same limitation on available abducibles, to generate a list of formulas meant to be part of the premise. We will later aggregate this list into a conjunction.

Next, we eliminate duplicates with Prolog’s sort/2.

We derive any_mints_premise/4 in a way similar to any_protasis/6, except that the arguments WithNeg and AggregatorOp become unnecessary and multiple occurrences of any abducible need to be supported. For brevity, we explain our steps as comments in the code.

Note that we have limited the length of the premise in the case of the Mints-formulas, arbitrarily, to the number of abducible atoms, that the selection of atoms has as an upper bound. For more flexibility, this can be lifted to be based on a length parameter passed to any_mints_premise.

4.2 Labeling the variables in the Mints formulas

We will describe here the implementation of part_as_equiv/2 that will be used to to generate variables bound to possibly repeated occurrences of each atom. Note that equalities of logic variables define equivalence classes that correspond to partitions of the set of variables. We implement this simply by selectively unifying them.

The predicate part_as_equiv/2 takes a list of distinct logic variables and generates partitions-as-equivalence-relations by unifying them “nondeterministically”. It also collects the unique variables defining the equivalence classes, as a list given by its second argument. It works reversibly, when unique values are given as its second argument and a bound list of free variables as its first.

To implement it, we split a set repeatedly in subset+complement pairs with help from the predicate complement_of/2.

We derive weakest_mints_premise/4 in a way similar to weakest_protasis/6 except for passing only the relevant arguments to any_mints_premise/4.

In fact, we observe:

suggesting that extending IL with:

|f v (f->g) v (g -> g)|

would result in an alternative axiomatization of the logic of here-and-there.