In this paper we describe an automated theorem prover for the intuitionistic non-Fregean sentential calculus with Suszko's identity ISCI. We first review the basic concepts of the logic, recall the recently proposed Topological Beth semantics for ISCI and a corresponding sound and complete labelled calculus. From this calculus we investigate automated proof search for ISCI and present the theorem prover AutoPSI through its architecture, its proof search strategies and optimizations. We complete with tests and benchmarks that illustrate the impact of strategies.
In this section, we recall the basic notions of ISCI [
A ::= P | ⊥ | A ∧ A | A ∨ A | A ⊃ A | A ≈ A (MP) From A and A ⊃ B deduce B.
In this work we use the Topological Beth (TB) semantics for ISCI and briefly review its main concepts
and results introduced in [
Definition 2. Let M be a set of elements, called worlds, such that ω, π ∈ M and ω ̸= π. A TB frame is a bounded distributive lattice ℱ = (M, ⩽, ⊔, ω, ⊓, π) with ω and π as least and greatest elements respectively.
Definition 3. A TB pre-model is a triple ℳ = (ℱ , [·], ⊩), where ℱ is a TB frame, and [·] is a valuation function from M to ℘(P ∪ F≈), such that for all worlds m and n: (ℳ (ℳ (ℳ (ℳ π) [π] = P ∪ F≈, K) if m ⩽ n then [m] ⊆ [n], ≈1 ) A ≈ A ∈ [m], • m ⊩ p iff p ∈ [m], • m ⊩ A ≈ B iff A ≈ B ∈ [m], • m ⊩ ⊥ iff π ⩽ m, • m ⊩ A ∧ B iff m ⊩ A and m ⊩ B, ≈4 ) for all ⊗ ∈ { ∧, ∨, ⊃, ≈ }, if A ≈ B, C ≈ D ∈ [m] then A ⊗ C ≈ B ⊗ D ∈ [m]. The forcing relation ⊩ is inductively defined as the smallest relation on M × F such that: • m ⊩ A ⊃ B iff for all n ∈ M, if n ⊩ A then m ⊔ n ⊩ B, • m ⊩ A ∨ B iff for some n1, n2 ∈ M such that n1 ⊓ n2 ⩽ m, n1 ⊩ A and n2 ⊩ B.
A TB model is a TB pre-model satisfying the admissibility condition: (ℳ ≈3 ) if m ⊩ A ≈ B then m ⊩ B ⊃ A.
Let us remark that ℳ π implies that all TB models have a world π that forces all formulas including ⊥. As usual, a formula A is true (or satisfied) in a TB model ℳ , written ℳ ⊨ A, iff m ⊩ A for all worlds m in ℳ and valid, written ⊨A, iff it is true in all models. It is routine to show that ℳ π and ℳ K extend from propositional letters and equations to all formulas. ℳ K is the well-known Kripke monotonicity condition, which applies to equations in our setting.
Definition 4. Let ℳ = (ℱ , [·], ⊩) be a TB model. ℳ is regular iff for all formulas A, if m ⊩ A for some world m, then there exists a world mA, called A-minimal, such that mA ⊩ A and for all worlds n, n ⊩ A implies mA ⩽ n. We write ⊨r for the restriction of validity to the class of regular TB models. Theorem 1 (Adequacy of regular Beth models). Regular TB models are HISCI-sound and HISCIcomplete: if ⊢HISCI A then ⊨r A, and if ⊨r A then ⊢HISCI A.
Since our prover AutoPSI implements the LISCI labelled calculus defined in [
The set L of labels is the union of the set N with all of its finite subsets. We use the (possibly subscripted or primed) letters a, b, c to denote singletons and save the letters x, y, z to denote arbitrary labels. A label x is a sublabel of a label y if x ⊆ y.
We work with a labelling algebra ℒ defined as the lattice (L, ⊆, ∪, ∅, ∩, N), where join ∪ and meet ∩ are standard set union and intersection. We consider that ∪ binds stronger than ∩ and we shall frequently write xy instead of x ∪ y (xx′ ∩ yy′ should therefore be read as (x ∪ x′) ∩ (y ∪ y′)). In this paper, we shall only use examples with label letters built from the subset { 1, . . . , 9 }. Therefore, we shall use the more concise notation 13 to unambiguously refer to { 1, 3 } (and not to the singleton { 13 }). Definition 5. A labelled formula is a pair (C, x), written C : x, where C is a formula and x is a label. A labelled sequent is a pair (Γ, Δ), written Γ ⊢ Δ, where Γ, Δ are sets of labelled formulas.
Given a set Δ of labelled formulas, the notation x ⊑ Δ means that x ⊆ y for some labelled formula A : y occurring in Δ. We write ⌈Δ⌉ for the set of all labels that are maximal in Δ: ⌈Δ⌉ = { z ⊑ Δ | if u ⊑ Δ and z ⊆ u then u = z }. Let s = Γ ⊢ Δ be a labelled sequent. A label x is right maximal in s if x ∈ ⌈Δ⌉ and s is right connected iff (∀ A : x ∈ Γ)(x ⊑ Δ).
The labelled calculus LISCI deals with labelled sequents Γ ⊢ Δ where Δ is not allowed to be empty. Some of the rules (⊥L, ∨L, ≈LL, ≈LR) have two principal formulas. In this case, one is called primarily principal and the other secondarily principal. In ≈LL and ≈LR, the equation that provides the substitution is primarily principal while the formula in which the substitution occurs is secondarily principal. In ⊥L and ∨L, the primarily principal formula is the one in the antecedent of the conclusion.
The rule ≈LL replaces (some, possibly all) occurrences of C in D with B and we write DBC as a shorthand for D[C/B]. Similarly for ≈LR with A instead of D. We call such substitutions sentential substitutions.
Definition 6. A formula A is a theorem of (or derivable in) LISCI, written ⊢LISCI A, if ⊢ A : ∅ is derivable in LISCI. Identity Rules: Core Intuitionistic Rules: Disjunction and Falsity Rules: Sentential Identity Rules:
idp(x ⊆ y) Γ, p : x ⊢ Δ, p : y Γ, A ≈ B : x ⊢ Δ, A ≈ B : y
id≈(x ⊆ y) Γ, B ⊃ C : x ⊢ Δ, B : z Γ, B ⊃ C : x, C : xz ⊢ Δ Γ, A : a ⊢ Δ, B : ya Γ ⊢ Δ, A ⊃ B : y ⊃R Γ, B ⊃ C : x ⊢ Δ Γ, B : x, C : x ⊢ Δ Γ, B ∧ C : x ⊢ Δ
⊃L(xz ⊑ Δ) ∧L Γ ⊢ Δ, A : y Γ ⊢ Δ, B : y Γ ⊢ Δ, A ∧ B : y ∧R Γ, ⊥ : x ⊢ Δ, A : y ⊥L(x ⊆ y) ΓΓ⊢⊢ΔΔ,,AA11:∨y,AA22::yy ∨R Γ, B ∨ C : x, B : xa1 ⊢ Δ, A : ya1 Γ, B ∨ C : x, C : xa2 ⊢ Δ, A : ya2 Γ, B ∨ C : x ⊢ Δ, A : y Γ, B ≈ C : x, C ⊃ B : x ⊢ Δ Γ, B ≈ C : x ⊢ Δ
≈L3 Γ, B ≈ C : x, D : x, DBC : x ⊢ Δ Γ, B ≈ C : x, D : x ⊢ Δ
≈LL Γ, B ≈ C : x ⊢ Δ, A : y, ABC : y Γ, B ≈ C : x ⊢ Δ, A : y Γ, B1 ≈ B2 : x, Bi ≈ Bi : x ⊢ Δ
Γ, B1 ≈ B2 : x ⊢ Δ ≈LR(x ⊆ y) Γ ⊢ Δ, A ≈ A : y ∨L(x ⊆ y)
≈LL′ ≈R Maximality Rule: Γ, B ⊃ C : x ⊢ Δ, B : xz Γ, B ⊃ C : x, C : xz ⊢ Δ Γ, B ⊃ C : x ⊢ Δ ⊃L(xz ∈ ⌈Δ⌉) Eigenvariable conditions: In ⊃R and ∨L, a, a1, a2 are fresh singletons and a1 ̸= a2.
A very important feature of LISCI, stemming from the use of Topological Beth semantics instead of Kripke semantics, is that it remains sound if the eigenvariable conditions are dropped. Therefore, when a labelled formula C : x requiring the introduction of fresh labels has to be expanded, one can reuse the labels that were generated during the first expansion of the formula C : x (or of any formula of the form C : y). The use of LISCI without the eigenvariable is called liberalized LISCI. Since AutoPSI is an implementation of liberalized LISCI, we only consider liberalized derivations in the remainder of the paper.
Theorem 2 (Liberalized soundness). If A is provable in liberalized LISCI then ⊢HISCI A. Example 2. Let us consider the following partial derivation for the non-valid formula ((p ∨ q) ⊃ p) ∨ ((p ∨ q) ⊃ q), where the second instance of ⊃R reuses the label 1 introduced by the first instance: p ∨ q : 1, p ∨ q : 1 ⊢ p : 1, q : 1 Π p ∨ q : 1 ⊢ p : 1, (p ∨ q) ⊃ q : ∅ ⊢ (p ∨ q) ⊃ p : ∅, (p ∨ q) ⊃ q : ∅ ⊢ ((p ∨ q) ⊃ p) ∨ ((p ∨ q) ⊃ q) : ∅ ⊃R ⊃R
∨R With a standard Kripke rule for left disjunction that would simply propagate the labels, we would get a proof for a non-valid formula as follows: □ • ⊥ ◁ A for all A ̸= ⊥, • if |A| < |B| then A ◁ B, and • if A ◁ B then C[A/B] ◁ C.
p ∨ q : 1, p : 1 ⊢ p : 1, q : 1 p ∨ q : 1, p ∨ q : 1 ⊢ p : 1, q : 1 idp
idp p ∨ q : 1, q : 1 ⊢ p : 1, q : 1 K ∨L The left premiss of the topmost instance of ∨L gives rise to the sequent s, in which p ∨ q : 1 can be reexpanded using either p : 12, or q : 13 in the succedent. Both choices reintroduce s as a premiss of ∨L making it impossible to reach an axiom as depicted below.
p ∨ q : 1, q : 13, p : 12 ⊢ p : 123, q : 12
p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 s p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 123 p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12
∨L idp ∨L idp
s p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12
Let us assume some fixed strict total Noetherian order ◁ on F such that: where |C| denotes the size of a formula C defined as the number of its connectives. Definition 7. rLISCI is LISCI under the following restrictions: (R1) Only equations can be secondarily principal for ≈LR and ≈LL. (R2) Equations of the form A ≈ A are never (primarily or secondarily) principal for ≈LR and ≈LL. (R3) ≈LR only performs strictly decreasing substitutions, i.e. if the rule replaces C with B in A then
ABC ◁ A. (R4) ≈LR and ≈LL only perform uniform substitutions, i.e., they make all possible replacements in the secondarily principal formula. (R5) ≈LR and ≈LL only perform substitutions that preserve the main connective of the secondarily principal formula.
Restrictions R1, R2 and R3 are required for the cut-elimination proof developped in [
Since all of the axioms and rules of HISCI are derivable in rLISCI and since cut can be eliminated from rLISCI, we have the following completeness result: Theorem 3 (Completeness under sentential restrictions). If ⊢HISCI A then A is provable in rLISCI, i.e., in LISCI with the restrictions of Definition 7. 1Irrelevant formulas are omitted to keep the proof in the page width. String
The completeness result can be further extended to proofs in which rules with principal formulas occurring in the succedent (right principal) are only allowed to be applied if their right principal formulas have a right maximal label. Such a rule application strategy is called right maximality Finally, a last important property of LISCI and rLISCI is that the set of provable formulas remains the same if one replaces the original rule for right implication with the maximality rule depicted in Fig. 2. Theorem 4 (Completeness under right maximality). If ⊢HISCI A then A is provable in LISCI or in rLISCI both restricted to the right maximality strategy.
In this section we present AutoPSI, an implementation of liberalized rLISCI written in Java. The parsing of the formulas is generated by ANTLR from the grammar described in Section 2. The Java application consists in 31 classes, 4 of them being automatically generated by ANTLR.
AutoPSI is available at https://homepages.loria.fr/dmery/autopsi. Let us note that a screen capture of an AutoPSI session is given in Appendix A.
The global architecture of AutoPSI is depicted in the execution diagram in Fig. 3. The input of the prover is a string representing the formula to prove, using the following grammar : • FORMULA : – (FORMULA) – FORMULA | FORMULA – FORMULA&FORMULA – FORMULA->FORMULA – FORMULA=FORMULA – ATOM – F (for ⊥) • ATOM : [a-z]* Algorithm 1: Global Approach
Input: s : string Data: S : Sequent(setof f ormulas); F : F ormula; P : P roof tree
Output: V : boolean 1 S ← ∅; 2 F ← P arse(s); 3 S ← S ∪ {F }; // Right-hand side of the sequent 4 P ← Compute(S, ∅); // Returns a proof tree 5 V ← IsAP roof (P ); // True iff all leaves are axioms 6 return V ; This string is parsed, creating an instance of the class Formula which is a syntactic tree of the formula. This formula is put into a sequent, which is a list of signed formulas (positive for the left-hand side, negative for the right-hand side). Then the majority of the computation is done by the class Calculus, which for every sequent starts by checking if it is an axiom, if it is an axiom then the computation stops, if not we need to apply a rule. The program then calls for a choice for the next formula in the sequent to decompose. This choice is made by a strategy that gives priorities to the available formulas. Once a formula is chosen, the program can check which rule to apply to the sequent depending on the formula. The application of this rule creates one or two new sequents in which the chosen formula is marked as used (except for the positive implications which can be used several times).
The Calculus class is designed to work with abstract classes for formulas, and interfaces for rules and strategies. This should allow us to reuse the core of the system for other sequent calculi.
Since AutoPSI is an implementation of LISCI, we need to deal with labelled formulas. Labels in LISCI are sets of integers that are implemented in AutoPSI as instances of the HashSet class in Java. This allows us to easily perform the inclusion tests required as side conditions by some of the rules like ⊃L, ∨L, the axiom rules and the sentential identity rules. From a technical point of view, inclusion is simply checked as inclusion between Java HashSet instances.
The mitigation of the eigenvariable condition is implemented in a singleton class that keeps track of all currently generated singleton labels. The singleton class allows singleton labels to be reused by considering them as minimal w.r.t. the formula they were firstly introduced with. Minimality is achieved by managing a dictionary whose keys are formulas and values are label letters. Whenever a formula requiring a fresh singleton label needs to be introduced in a sequent, for instance when applying the rule ∨L to a labelled formula A ∨ B : x, we first check whether the dictionary already contains a key-value pair A : ai (meaning that ai is A-minimal). If so, the singleton ai is reused and A : ai is inserted in the antecedent of the current sequent. Otherwise, a fresh label letter aj is generated by the singleton class and associated with A is the dictionary for later reuse before inserting A : aj in the current sequent.
Given a formula as input, AutoPSI explores the proof search space using a depth-first search policy. During the exploration, the prover keeps track of all the rules that have been applied previously (as well as the formulas on which they were applied) in a tree structure called the rule-tree. To reduce the memory footprint, the sequents themselves are not explicitly stored in the rule-tree but can be recovered from the input formula by replaying all the rules up to a given point. If all the leaves of the rule-tree are axioms (zero-premiss rules) the input formula is deemed valid. In this case, the rule-tree can be converted to an actual proof tree (with all of its intermediate sequents as its nodes) if needed. Otherwise, if all possible rules have already been applied and all backtracking points have been exhausted, the input formula is deemed non-valid. The global approach and the detailed pseudo code of the proof Algorithm 2: Compute
Input: S : Sequent(Setof f ormulas); P : P roof T ree Data: S1, S2 : Sequent(setof f ormulas); F, F R : F ormula; P1, P2 : P roof tree; Rules : Rule[]; R : Rule
Output: P : P roof tree 1 if S is not an axiom then 2 F ← Choose(S); // A formula is chosen for the derivation 3 Rules ← Rule(F ); 4 foreach R in Rules do 5 if R needs a choice on the right then 6 i ← 0; 7 while P1 is null and i < Size(SR) do // We check all possible choices until we find a proof F R ← SR(i); // of the right formulas of S < S1, S2 >← Apply(R, S, F, F R); P1 ← Compute(P, S1); if IsAP roof (P1) then
P2 ← Compute(P, S2); if IsAP roof (P2) then
P ← Compose(P1, P2, P ); // We merge the proof trees end else end end else
P1, P2 ← null;
P1, P2 ← null; end i ← i + 1; end return P ; end else // R does not need a choice < S1, S2 >← Apply(R, S, F, F R); P1 ← Compute(∅, S1); P2 ← Compute(P, S2); P ← Compose(P1, P2, P ); // We merge the proof trees return P ; search procedure are given in Algorithms 1 and 2. In Algorithm 2, the only data that we keep track of is the order of application of the rules in the proof, that we call a Proof Tree. This allows the prover to only deal with one sequent at a time, while still having the information needed to build the proof if asked to. The while loop starting on line 7 states that we check every possible choice for the proof until we either find a proof, or we have checked every suitable formula for this rule application. For example, if the choices for the secondarily principal formula are between formulas A and B, then we start with formula A first. If the proof is completed, we stop there, if not, the Proof Tree will be null, then the loop will go on and try with B. When the proof is completed, the use of the predicate Compose on lines 14 and 31 will merge the Proof Trees (the two trees created by the rule application, P1 and P2, and the former one that represents the proof below, P, into the new Proof Tree P) and we will get an axiom at the top of the Proof Tree. Then the call to the procedure IsAProof in line 5 of algorithm 1 will return true.
AutoPSI implements all of the restrictions described in Definition 7 and further restricts ≈LL to
sentential substitutions bounded by the size of the initial formula to prove which is called the degree of
the proof. Let us remark that such a restriction is proven complete for SCI in [
A first optimization, called subsumption, takes advantage of Kripke monotonicity (condition ℳ K of Definition 3) to subsume formulas on both sides of a sequent and thus prevent them from being expanded. More precisely, a positive formula A : y is considered subsumed (and thus prevented from expansion) if the current sequent already contains a positive formula A : x such that x ⊆ y. Similarly for negative formulas such that y ⊆ x. Since we create a finite number of formulas and labels, subsumption is not needed for termination. That is because the prover works with sets of formulas and if a formula is already in the set, it is not added to the sequent, but subsumption will limit the number of useless decompositions in the proof.
A second optimization is that we put an upper bound on the number of times positive implications can be reused to ensure that they do not get expanded infinitely often by ⊃L. This upper bound is called “Time to Live” (TTL) and is implemented as a counter that is equal to the sum of the number of negative implications and twice the number of positive disjunctions occurring in a sequent as those rules are the only ones that might generate fresh singletons. LISCI does not enjoy the subformula property (in its strict acception) since sentential substitutions might generate subformulas that did not occur in the initial formula to prove. Therefore, the TTL is updated dynamically during the proof search process when new singletons are generated.
Theorem 5. The proof system LISCI in which positive implications are not used more times than their TTL is complete.
Proof. When a positive implication is decomposed, there is a list of candidates for the formula on the right-hand side, which are the formulas with bigger labels than the implication being decomposed. In this selection of candidates, there are maximal formulas, i.e. formulas that have labels that are not smaller than any other label on the right-hand side. The prover will try with one formula and if it does not find a proof, it will backtrack to try with another candidate. Then it will eventually use a maximal formula as a secondarily principal formula. Since the system that uses maximality is complete, this step does not prevent completeness. Then, if the implication is decomposed again in the proof, the prover will try a new candidate if and only if there is a new label, that means if a new label atom has been introduced since the last decomposition. Then, each positive implication can be decomposed at most a number of times that is equal to the number of labels created in the proof, that is the formula’s TTL. □ 5.2.2. Strategies At each step of the exploration, the prover needs to choose the next formula to be expanded (called the principal formula). This task is devoted to an object called a strategy which implements the Strategy interface. Every time a rule is decomposed, the principal formula is marked as being used, with the exception of the implications on the left-hand side of the sequent that can be used several times. The rule application strategy used in AutoPSI is to delay choices as long as possible. There are two kinds of choices: the ones that involve the guessing of labels satisfying some side conditions as it is the case for the rule ⊃L and the ones that involve the choice of a secondarily principal formula as it is the case for the rules ∨L, ≈LL and ≈LR. Making the right choices for secondarily principal formulas is the biggest performance issue that the prover currently faces. The number of suitable formulas can be large and when a formula is not valid we have to explore every possible choice before failing eventually.
Our first strategy is called “First One Strategy”. In this strategy, the prover decomposes formulas in their order of apparition in the sequent, the older ones having priority. This strategy is not complete.
Our second strategy is called “New Labels First”. It gives precedence to the rules that introduce new labels in the proof, such as ⊃R and ∨L, in order to have them ready for occurrences of positive implications and right-handed substitutions that need bigger labels in their right-principal formula. The rules that require choices and do not create labels, like ⊃L and all identity rules are chosen last, in order to delay choices higher in the proof. For the choice of secondarily principal formulas, the candidates are ordered by increasing size, with the hope that a small formula should be less likely to create a big number of branches and nodes. Therefore, in the case that such a choice should eventually fail, backtracking to the next one would not cost as much as for a bigger formula.
A third strategy is called “Partial Δ-Maximality”. It uses the same priorities as the “New Labels First” strategy, but it only allows the rules ⊃L, ∨L, ≈LL and ≈LR to be expanded with secondarily principal formulas having right-maximal labels. It is therefore an implementation of the maximality strategy discussed in Section 4. Choosing formulas with right maximal labels reduces the number of candidates. For other rules, the strategy can still use non left-maximal formulas.
More clever strategies for the choice of secondarily principal formulas shall be studied as future work. One improvement to make better choices, inspired by connection methods, would be to aim for candidates that actually contain atoms that could be complementary with the primarily principal formula. One difficulty w.r.t. connection methods is that LISCI does not enjoy the subformula property, so that complementarity cannot be precomputed once and for all before starting the proof search process and should be done on the fly.
Example 3. Let us consider the formula ¬¬(A ∨ ¬A). Negation is not a native rule in LISCI, so our starting formula is in fact ((A ∨ (A ⊃ ⊥)) ⊃ ⊥) ⊃ ⊥, which contains two negative implications and no positive disjunctions. Therefore, AutoPSI should be allowed to expand the same positive implication at most twice.
After the creation of the labelled sequent ⊢ ((A ∨ (A ⊃ ⊥)) ⊃ ⊥) ⊃ ⊥ : ∅, only one formula can be selected by the rule application strategy: the one in the succedent. After the rule ⊃R is applied we get the sequent (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1 ⊢ ⊥ : 1 (for conciseness we do not keep expanded formulas). The only selectable formula is a positive implication. After ⊃L is applied we get the following premises. (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1 ⊢ ⊥ : 1, A ∨ (A ⊃ ⊥) : 1 (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, ⊥ : 1 ⊢ ⊥ : 1 (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1 ⊢ ⊥ : 1 ⊃L
The second premiss is the axiom ⊥L so its exploration stops successfully. The first one still needs to be explored further. We have now the choice between two rules, ⊃L (still usable) and ∨R. The rule application strategy puts the priority on ∨R, resulting in the sequent (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1 ⊢ ⊥ : 1, A : 1, A ⊃ ⊥ : 1.
Now have the choice between ⊃L or ⊃R and the rule application strategy selects ⊃R. The resulting sequent is (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12 which is not an axiom yet but we can reuse the rule ⊃L to get two subproofs reaching axioms: Π1 (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12, A ⊃ ⊥ : 12, A : 12 (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12, A ∨ (A ⊃ ⊥) : 12 id ∨R Π2 n (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2, ⊥ : 12 ⊢ ⊥ : 1, A : 1, ⊥ : 12 ⊥L
Several indicators are built in AutoPSI to evaluate its efficiency. The first one is obviously the validity status (St) of the input formula (T for valid, F for invalid). The second one is the execution time measured in milliseconds (Tms). The third and fourth ones are the maximum depth and the size of the search space explored by the prover respectively measured as the maximum depth (D) and the number of nodes (N) in the rule-tree structure. We also measure the number of branches created (B). For valid formulas we also count the number of nodes in the final proof (Np) and its depth (Dp). In the case of a valid formula, the ratio between the size of the proof Np and the size of the search space N gives an account of the optimality of the proof search strategy: if N is significantly greater than Np then AutoPSI explored many wrong choices before making the right ones.
As AutoPSI is the first prover for ISCI, we do not have any other tool to compare it with. There is no
substantial test base for ISCI, we thus derive our tests from the Φ formula introduced in [
Φ is valid in SCI but it is not valid in ISCI, therefore we will try to prove ¬Φ and ¬¬Φ as well, with the later expected to be valid thanks to the double negation. We will also study Ψ, which is Ψ but with identities instead of equivalences:
Ψ ≡ (((q ≈ p) ⊃ (p ⊃ r)) ≈ ((p ⊃ (p ≈ p)) ≈ p)) ⊃ (((r ∧ p) ≈ (p ≈ p)) ∨ ((p ∧ p) ∨ ¬q)) This transformation is not valid since two equivalent formulas are not necessarily identical. The column TTL stands for “Time To Live” and indicates the maximum number of expansions allowed for positive implications. Finally, we add χ: χ ≡ (((p ∧ (q ⊃ q2)) ≈ (p ∧ (q ⊃ q2))) ∧ (((p ∧ (q ⊃ q2)) ≈ (r ∨ p2)) ≈ (p ∧ (q ⊃ q2)))) ⊃ ((p ∧ (q ⊃ q2)) ≈ (r ∨ p2))
Since ISCI is a conservative extension of IL, we complete our test base with three purely intuitionistic formulas:
F1 ≡ ((((p ⇔ q) ∨ (p ⇔ r)) ∨ (q ⇔ r)) ⊃ ((p ∧ q) ∧ r)) ⊃ ((p ∧ q) ∧ r) F2 ≡ (¬¬(¬p ⊃ q)) ⊃ ((¬p ⊃ ¬q) ⊃ p) F3 ≡ ¬¬((((q ⊃ p) ⊃ (p ⊃ r)) ⊃ ((p ⊃ ((p ⊃ p) ∧ (p ⊃ p))) ⊃ p))
⊃((((r ∧ p) ⊃ (p ⊃ p)) ∧ (p ⊃ p) ⊃ (r ∧ p))) ∨ ((p ∧ p) ∨ ¬q)) Form Φ ¬Φ ¬¬Φ False
¬¬¬Φ False 10 10 9 6 7 7 8 8 9 8 6 False
¬¬Ψ
False ¬¬χ
True Ψ ¬Ψ χ ¬χ F1 F2 F3 great improvement to find an efficient heuristic for guessing the right secondarily principal formulas since exploring too many wrong choices might take too long for big formulas. One formula we can not solve right now is ¬¬Φ, which is not valid but the prover must explore too many branches to terminate in a reasonable amount of time.
Despite not being able to solve ¬¬Φ, the strategy improves the prover on most of the formulas. The only formula where we have a worst case in execution time is ¬χ, because despite having a smaller search tree, the management of maximal formulas is time consuming and here it is not compensated 13 13 13 9 9 9 27 27 6 5 5 21 21 48 15 15 35 38 26 25 80 30 enough to improve the execution. This is the same reason why we improve the execution time of ¬¬¬Φ by only two seconds despite dividing the size of the search tree by two. All other formulas are improved by the maximality strategy. In particular, tests done on purely intuitionistic formulas show that maximality is an interesting optimization for our prover.
Since ISCI is a conservative extension of IL, AutoPSI is also an automated theorem prover for IL.
However, let us remark that AutoPSI is currently not a competitive tool for IL, even when compared to
our old STRIP prover [
The prover AutoPSI is the first automated prover for the logic ISCI. AutoPSI is based on the system LISCI, a labelled multi-conclusioned sequent calculus system, based on the Topological Beth semantics. The prover uses properties of both LISCI and the Topological Beth semantics to enhance its performances. These properties are the regularity of the Topological Beth models, allowing the prover to have a finite search space, the maximality of the proof system, which enables the prover to terminate. Other properties are optimizations, like the restrictions on the identity rules allowed by our proof system, the subsumption of formulas that are not useful in the proof, and the maximality property of our proof system that allows to disregard some formulas that are not maximal in some steps of the proof. The last two optimizations are tested on a test base of several ISCI and IL formulas. The tests demonstrate the usefulness of such optimizations, as well as the difficulties of the prover on the restriction to IL. These difficulties are explained by the design of the proof system, built to deal with the identity operator.
Future works will focus on more optimizations for AutoPSI, mostly by implementing and testing other strategies. One strategy that could be really interesting is a strategy that uses the full maximality property, on every step of the proof and not just some steps. Such a strategy could drastically improve the prover performances.