In this paper we consider the intuitionistic sentential calculus with identity (ISCI) which extends intuitionistic logic with Suszko's identity operator ≈ introduced in [1] for non-Fregean logics. In the non-Fregean approach identity and logical equivalence have distinct meanings: two sentences with the same truth value can have different denotations. For example, two logically equivalent formulas might have distinct sets of proofs. Suszko's identity has been studied as an extension of classical logic in [2]. The resulting logic is called SCI. The intuitionistic variant ISCI has been studied in [3] and we have recently proposed a new semantics, called Topological Beth semantics and a new sequent-style labelled calculus L ISCI for ISCI in [4]. From these results we study automated proof search in this logic and present the theorem prover AutoPSI through its architecture and its proof search strategies and optimizations. Tests and benchmarks complete this study.
In this section, we recall the basic notions of ISCI [2,1]. ISCI extends propositional intuitionistic logic (IL) with axioms that formalize the non-truth functional nature of the identity connective ≈. Definition 1. Let P = { p, q, . . . } be a countable set of propositional letters. The formulas of ISCI, the set of which is denoted F, are given by the grammar:
Formulas of the form A ≈ B are called equations. We write F ≈ for the restriction of F to equations. Negation ¬A and truth ⊤ are respectively defined as A ⊃ ⊥ and ⊥ ⊃ ⊥.
ISCI can be axiomatized by adding the four identity axioms described in Fig. 1 to any axiom schemata for IL [2]. We call "H ISCI " the Hilbert proof system consisting of the four axioms for identity, the ten axioms for IL and the rule of modus ponens. We write S ⊢HISCI B to mean that a formula B is derivable in H ISCI from a finite set S = { A 1 , . . . , A n } of assumptions. Whenever S is empty, B is called a thesis or a theorem of H ISCI . Let us note that the deduction theorem holds for H ISCI , i.e. A 1 , . . . , Example 1. The following is an H ISCI proof that ≈ is commutative, more precisely, we show A ≈ B ⊢HISCI B ≈ A:
In this work we use the Topological Beth (TB) semantics for ISCI and briefly review its main concepts and results introduced in [4].
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.
, where ℱ is a TB frame, and [•] is a valuation function from M to ℘(P ∪ F ≈ ), such that for all worlds m and n:
The forcing relation ⊩ is inductively defined as the smallest relation on M × F such that:
A TB model is a TB pre-model satisfying the admissibility condition:
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.
for some world m, then there exists a world m A , called A-minimal, such that m A ⊩ A and for all worlds n, n ⊩ A implies m A ⩽ 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 H ISCI -sound and H ISCIcomplete: if ⊢HISCI A then ⊨r A, and if ⊨r A then ⊢HISCI A.
Since our prover AutoPSI implements the L ISCI labelled calculus defined in [4] (more precisely the L 2 ISCI variant of the calculus), let us briefly recall its basic concepts.
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 ∆:
The labelled calculus L ISCI 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 D C B 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) L ISCI , written
Disjunction and Falsity Rules:
Eigenvariable conditions: In ⊃ R and ∨ L , a, a 1 , a 2 are fresh singletons and a 1 ̸ = a 2 . A very important feature of L ISCI , 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 L ISCI without the eigenvariable is called liberalized L ISCI . Since AutoPSI is an implementation of liberalized L ISCI , we only consider liberalized derivations in the remainder of the paper.
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:
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:
On the contrary, in L ISCI , applying the Beth rule for left disjunction we get1 : idp p ∨ q : 1, p : 12 ⊢ p : 12 s p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 idp p ∨ q : 1, q : 13 ⊢ q : 13 ∨L p ∨ q : 1, q : 13 ⊢ p : 13, q : 1 ∨L p ∨ q : 1, p ∨ q : 1 ⊢ p : 1, q : 1
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. idp p ∨ q : 1, q : 13, p : 12 ⊢ p : 123, q : 12 s p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 ∨L p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 s p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 idp p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 123 ∨L 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. (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 [4]. The other restrictions are not mandatory but they simplify the implementation of the AutoPSI theorem prover. Let us remark that R1 guarantees that sentential substitutions should only occur inside equations, while R5 guarantees that equations should remain equations after a sentential substitution.
Since all of the axioms and rules of H ISCI are derivable in rL ISCI and since cut can be eliminated from rL ISCI , we have the following completeness result: 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 L ISCI and rL ISCI 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.
If ⊢HISCI A then A is provable in L ISCI or in rL ISCI both restricted to the right maximality strategy.
In this section we present AutoPSI, an implementation of liberalized rL ISCI 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 : 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 L ISCI , we need to deal with labelled formulas. Labels in L ISCI 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 : a i (meaning that a i is A-minimal). If so, the singleton a i is reused and A : a i is inserted in the antecedent of the current sequent. Otherwise, a fresh label letter a j is generated by the singleton class and associated with A is the dictionary for later reuse before inserting A : a j 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 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 ProofTree. 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 ProofTree 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 ProofTrees (the two trees created by the rule application, P1 and P2, and the former one that represents the proof below, P, into the new ProofTree P) and we will get an axiom at the top of the ProofTree. 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 [5]. In the case of ISCI the completeness result is only achieved, via counter-model construction, for a fragment where formulas are syntactically restricted to implications and identities only [6], but not for the full logic. A current limitation of AutoPSI is that it cannot generate a counter-model in case of non-validity.
Following the terminology of one-sided sequents, we assign a polarity to each formula occurring in a labelled sequent: positive if it occurs in the antecedent and negative if it occurs in the succedent.
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. L ISCI 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 L ISCI 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. □
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 L ISCI 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 L ISCI , 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.
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:
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 [5], where a tableau prover for SCI (an extension of classical logic with the identity) is described:
We recall that negation ¬A and logical equivalence A ⇔ B have no specific rules in AutoPSI since they are only shorthands for A ⊃ ⊥ and (A ⊃ B) ∧ (B ⊃ A).
Φ 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:
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 χ:
Since ISCI is a conservative extension of IL, we complete our test base with three purely intuitionistic formulas:
Table 2 summarizes the results of running AutoPSI on the ISCI test base in different conditions. Firstly without the subsumption optimization and without the maximality strategy, then with the subsumption optimization but without the maximality strategy, and finally with both the subsumption optimization and the maximality strategy.
It is clear that the subsumption optimization drastically improves the efficiency of the prover. Without it, most of the formulas in the test base cannot be decided in a reasonable amount of time. What the formula ¬¬Φ shows us is that we explore too much, and that is mainly because of the rules ⊃ L , ∨ L , ≈ LL and ≈ LR , since we need to test all of their potential secondarily principal formulas. It would be a 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 [7]. The inefficiency comes from the use of Topological Beth semantics and its requirement to have rules with secondarily principal formulas. For IL, Kripke semantics is simpler and more efficient since one has the subformula property and various ways to tame the introduction of new labels. AutoPSI is firstly and mainly designed for ISCI, which does not enjoy the subformula property so that Topological Beth semantics is for the moment the easiest way to allow label reuse.
The prover AutoPSI is the first automated prover for the logic ISCI. AutoPSI is based on the system L ISCI , a labelled multi-conclusioned sequent calculus system, based on the Topological Beth semantics. The prover uses properties of both L ISCI 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.
Input: S : Sequent(Setof f ormulas); P : P roof T ree Data: S 1 , S 2 : Sequent(setof f ormulas); F, F R : F ormula; P 1 , P 2 : 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 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 A. AutoPSI Session Capture