=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper3
|storemode=property
|title=Automated Proof Search in Intuitionistic Sentential Logic
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper3.pdf
|volume=Vol-3875
|authors=Didier Galmiche,Brandon Hornbeck,Daniel Méry
|dblpUrl=https://dblp.org/rec/conf/arqnl/GalmicheHM24
}}
==Automated Proof Search in Intuitionistic Sentential Logic==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper3.pdf
Automated Proof Search in Intuitionistic Sentential Logic.
Didier Galmiche1 , Brandon Hornbeck1 and Daniel Méry1
1
Université de Lorraine, CNRS, LORIA Vandoeuvre-lès-Nancy, F-54506, France
Abstract
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.
Keywords
Automated Proof Search, Labelled Calculi, Non Fregean Logic, Intuitionistic Logic with Identity
1. Introduction
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 LISCI 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.
2. Intuitionistic Sentential Calculus with Identity
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:
A ::= P | ⊥ | A ∧ A | A ∨ A | A ⊃ A | A ≈ A
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 “HISCI ” 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 HISCI from a finite set S = { A1 , . . . , An } of assumptions. Whenever S is empty, B is called a thesis
or a theorem of HISCI . Let us note that the deduction theorem holds for HISCI , i.e. A1 , . . . , An ⊢ HISCI B
iff ⊢ HISCI A1 ∧ . . . ∧ An ⊃ B.
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
∗
Corresponding author.
†
These authors contributed equally.
$ didier.galmiche@loria.fr (D. Galmiche); brandon.hornbeck@loria.fr (B. Hornbeck); daniel.mery@loria.fr (D. Méry)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
ceur-ws.org
ISSN 1613-0073 ARQNL 2024 24 P ROCEEDINGS
Proceedings
(≈1 ) A≈A
(≈2 ) (A ≈ B) ⊃ (¬A ≈ ¬B)
(≈3 ) (A ≈ B) ⊃ (B ⊃ A)
(≈4 ) (A ≈ B) ∧ (C ≈ D) ⊃ (A ⊗ C) ≈ (B ⊗ D) where ⊗ ∈ { ∧, ∨, ⊃, ≈ }
(IL1 ) A ⊃ (B ⊃ A) (IL2 ) (A ⊃ B) ⊃ ((A ⊃ (B ⊃ C)) ⊃ (A ⊃ C))
(IL3 ) A ⊃ (B ⊃ (A ∧ B)) (IL4 ) (A ∧ B) ⊃ A
(IL5 ) (A ∧ B) ⊃ B (IL6 ) (A ⊃ C) ⊃ ((B ⊃ C) ⊃ ((A ∨ B) ⊃ C))
(IL7 ) A ⊃ (A ∨ B) (IL8 ) B ⊃ (A ∨ B)
(IL9 ) (A ⊃ B) ⊃ ((A ⊃ ¬B) ⊃ ¬A) (IL10 ) ¬A ⊃ (A ⊃ B)
(MP) From A and A ⊃ B deduce B.
Figure 1: Axioms for ISCI.
Example 1. The following is an HISCI proof that ≈ is commutative, more precisely, we show A ≈ B ⊢ HISCI
B ≈ A:
(1) A≈B assumption
(2) B≈B ≈1
(3) ((B ≈ B) ∧ (A ≈ B)) ⊃ ((B ≈ A) ≈ (B ≈ B)) ≈4
(4) (B ≈ B) ⊃ ((A ≈ B) ⊃ ((B ≈ B) ∧ (A ≈ B))) IL3
(5) (A ≈ B) ⊃ ((B ≈ B) ∧ (A ≈ B)) MP 2, 4
(6) (B ≈ B) ∧ (A ≈ B) MP 1, 5
(7) (B ≈ A) ≈ (B ≈ B) MP 3, 6
(8) ((B ≈ A) ≈ (B ≈ B)) ⊃ ((B ≈ B) ⊃ (B ≈ A)) ≈3
(9) (B ≈ B) ⊃ (B ≈ A) MP 7, 8
(10) B≈A MP 2, 9
□
3. Semantics for ISCI
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.
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],
(ℳ≈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 ⊩ p iff p ∈ [m],
• m ⊩ A ≈ B iff A ≈ B ∈ [m],
• m ⊩ ⊥ iff π ⩽ m,
• m ⊩ A ∧ B iff m ⊩ A and m ⊩ B,
25
• 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 HISCI -
complete: if ⊢ HISCI A then ⊨ r A, and if ⊨ r A then ⊢ HISCI A.
4. Labelled Deduction for ISCI
Since our prover AutoPSI implements the LISCI labelled calculus defined in [4] (more precisely the L2ISCI
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 ∆: ⌈∆⌉ = { 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 DC 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) LISCI , written ⊢ LISCI A, if ⊢ A : ∅ is derivable
in LISCI .
26
Identity Rules:
idp (x ⊆ y) id≈ (x ⊆ y)
Γ, p : x ⊢ ∆, p : y Γ, A ≈ B : x ⊢ ∆, A ≈ B : y
Core Intuitionistic Rules:
Γ, B ⊃ C : x ⊢ ∆, B : z Γ, B ⊃ C : x, C : xz ⊢ ∆
⊃L (xz ⊑ ∆)
Γ, B ⊃ C : x ⊢ ∆
Γ, A : a ⊢ ∆, B : ya Γ, B : x, C : x ⊢ ∆ Γ ⊢ ∆, A : y Γ ⊢ ∆, B : y
⊃R ∧L ∧R
Γ ⊢ ∆, A ⊃ B : y Γ, B ∧ C : x ⊢ ∆ Γ ⊢ ∆, A ∧ B : y
Disjunction and Falsity Rules:
⊥L (x ⊆ y) Γ ⊢ ∆, A1 : y, A2 : y ∨
Γ, ⊥ : x ⊢ ∆, A : y Γ ⊢ ∆, A1 ∨ A2 : y
R
Γ, B ∨ C : x, B : xa1 ⊢ ∆, A : ya1 Γ, B ∨ C : x, C : xa2 ⊢ ∆, A : ya2
∨L (x ⊆ y)
Γ, B ∨ C : x ⊢ ∆, A : y
Sentential Identity Rules:
Γ, B ≈ C : x, C ⊃ B : x ⊢ ∆
≈L3
Γ, B ≈ C : x ⊢ ∆
Γ, B ≈ C : x, D : x, DC
B :x ⊢ ∆ Γ, B1 ≈ B2 : x, Bi ≈ Bi : x ⊢ ∆
≈LL ≈LL′
Γ, B ≈ C : x, D : x ⊢ ∆ Γ, B1 ≈ B2 : x ⊢ ∆
Γ, B ≈ C : x ⊢ ∆, A : y, AC
B :y ≈R
≈LR (x ⊆ y) Γ ⊢ ∆, A ≈ A : y
Γ, B ≈ C : x ⊢ ∆, A : y
Maximality Rule:
Γ, B ⊃ C : x ⊢ ∆, B : xz Γ, B ⊃ C : x, C : xz ⊢ ∆
⊃L (xz ∈ ⌈∆⌉)
Γ, B ⊃ C : x ⊢ ∆
Eigenvariable conditions: In ⊃R and ∨L , a, a1 , a2 are fresh singletons and a1 ̸= a2 .
Figure 2: Rules for the LISCI Labelled Sequent Calculus.
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
⊃R
p ∨ q : 1 ⊢ p : 1, (p ∨ q) ⊃ q : ∅
Π ⊃R
⊢ (p ∨ q) ⊃ p : ∅, (p ∨ q) ⊃ q : ∅
∨R
⊢ ((p ∨ q) ⊃ p) ∨ ((p ∨ q) ⊃ q) : ∅
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:
27
idp idp
p ∨ q : 1, p : 1 ⊢ p : 1, q : 1 p ∨ q : 1, q : 1 ⊢ p : 1, q : 1
∨K
L
p ∨ q : 1, p ∨ q : 1 ⊢ p : 1, q : 1
On the contrary, in LISCI , applying the Beth rule for left disjunction we get1 :
s
idp
p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 p ∨ q : 1, q : 13 ⊢ q : 13
idp ∨L
p ∨ q : 1, p : 12 ⊢ p : 12 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.
s
idp
p ∨ q : 1, q : 13, p : 12 ⊢ p : 123, q : 12 p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12
∨L
p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12
s
idp
p ∨ q : 1, q : 13, p : 12 ⊢ p : 13, q : 12 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 Nœtherian order ◁ on F such that:
• ⊥ ◁ A for all A ̸= ⊥,
• if |A| < |B| then A ◁ B, and
• if A ◁ B then C[A/B] ◁ C.
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
AC
B ◁ 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 [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 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.
1
Irrelevant formulas are omitted to keep the proof in the page width.
28
Calculus ISCI
Strategies
String Sequent
Strat1
...
Parser yes axiom? no
finds nothing
found
Stop
Formula Formula
Rules
orL
Stop
...
Figure 3: Execution diagram
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.
5. AutoPSI: a Prover for ISCI
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.
5.1. Prover Architecture
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]*
29
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.
5.2. Proof Search, Optimizations and Strategies
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
30
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
8 F R ← SR (i); // of the right formulas of S
9 < S1 , S2 >← Apply(R, S, F, F R);
10 P1 ← Compute(P, S1 );
11 if IsAP roof (P1 ) then
12 P2 ← Compute(P, S2 );
13 if IsAP roof (P2 ) then
14 P ← Compose(P1 , P2 , P ); // We merge the proof trees
15 end
16 else
17 P1 , P2 ← null;
18 end
19 end
20 else
21 P1 , P2 ← null;
22 end
23 i ← i + 1;
24 end
25 return P ;
26 end
27 else
// R does not need a choice
28 < S1 , S2 >← Apply(R, S, F, F R);
29 P1 ← Compute(∅, S1 );
30 P2 ← Compute(P, S2 );
31 P ← Compose(P1 , P2 , P ); // We merge the proof trees
32 return P ;
33 end
34 end
35 end
36 else
// S is an Axiom
37 return P ;
38 end
31
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.
5.2.1. Optimizations
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. 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. □
32
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
⊃L
(A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1 ⊢ ⊥ : 1
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:
33
id
(A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12, A ⊃ ⊥ : 12, A : 12
Π1 ∨R
(A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12, A ∨ (A ⊃ ⊥) : 12
Π2 (A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2, ⊥ : 12 ⊢ ⊥ : 1, A : 1, ⊥ : 12 ⊥L
n
Π1 Π2
⊃L
(A ∨ (A ⊃ ⊥)) ⊃ ⊥ : 1, A : 2 ⊢ ⊥ : 1, A : 1, ⊥ : 12
□
5.3. Tests and Benchmarks
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:
Φ ≡ (((q ≈ p) ⊃ (p ⊃ r)) ≈ ((p ⊃ (p ⇔ p)) ≈ p)) ⊃ (((r ∧ p) ⇔ (p ≈ p)) ∨ ((p ∧ p) ∨ ¬q))
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:
Ψ ≡ (((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))
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
34
Form St TTL Conditions T(ms) D N B DP NP
(1) - - - - - -
Φ False 10 (2) 156.88 20 12185 6086 - -
(3) 52.00 20 30476 1734 - -
(1) 10.57 11 1025 512 - -
¬Φ False 9 (2) 2.29 11 219 109 - -
(3) 2.72 11 219 109 - -
(1) - - - - - -
¬¬Φ - - (2) - - - - - -
(3) - - - - - -
(1) - - - - - -
¬¬¬Φ False 10 (2) 15461 24 597142 297429 - -
(3) 9409 24 266422 133208 - -
(1) 5.44 13 321 306 - -
Ψ False 6 (2) 3.9 13 539 265 - -
(3) 0.46 13 57 26 - -
(1) 1.34 9 231 115 - -
¬Ψ False 7 (2) 0.58 9 83 41 - -
(3) 0.07 9 83 41 - -
(1) - - - - - -
¬¬Ψ False 7 (2) 14071 27 749390 353560 - -
(3) 2412 27 84720 27 - -
(1) 0.12 6 9 1 6 7
χ True 8 (2) 0.07 5 7 1 5 6
(3) 0.60 5 6 1 5 6
(1) - - - - - -
¬χ False 8 (2) 12172 21 851894 483465 - -
(3) 17836 21 851517 425757 - -
(1) 23.10 48 92 10 48 58
¬¬χ True 9 (2) 43.3 15 1556 748 7 9
(3) 4.84 15 144 69 7 9
(1) - - - - - -
F1 True 8 (2) 121.21 35 5697 1894 35 1374
(3) 41.90 38 1512 338 38 1512
(1) - - - - - -
F2 False 6 (2) 22470 26 2689430 1211098 - -
(3) 514.00 25 52751 26369 - -
(1) - - - - - -
F3 True 12 (2) 62831 80 790190 271515 80 246895
(3) 18.3 30 698 207 30 698
D = max depth explored, N = Number of nodes explored, B = Branches created,
DP = Depth of the proof, NP = Nodes in the proof
(1) = Without subsumption and without maximality
(2) = With subsumption and without maximality
(3) = With subsumption and with maximality
Table 2
AutoPSI tested in several conditions.
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
35
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.
Conclusion and future work
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.
References
[1] R. Suszko, Abolition of the Fregean axiom, in: Logic Colloquium, 1975, pp. 169–239. Springer.
[2] P. Lukowski, Intuitionistic sentential calculus with identity, Bulletin of the Section of Logic 19
(1990) 92–99.
[3] S. Chlebowski, D. Leszcyńska-Jasion, An Investigation into Intuitionistic Logic with Identity,
Bulletin of the Section of Logic 48 (2019) 259–283.
[4] D. Galmiche, M. Gawek, D. Méry, Beth semantics and labelled deduction for intuitionistic sentential
calculus with identity, in: 6th International Conference on Formal Structures for Computation and
Deduction, FSCD 2021, LIPIcs 195, Buenos Aires, Argentina, 2021, p. 13:1–13:21.
[5] J. Golińska-Pilarek, T. Huuskonen, M. Zawidzki, Tableau-based decision procedure for non-fregean
logic of sentential identity, in: 28th Int. Conference on Automated Deduction, CADE 2021, LNAI
12699, 2021, pp. 41–57.
[6] A. Tomczyk, D. Leszcyńska-Jasion, Decidability of Intuitionistic Sentential Logic with Identity
via Sequent Calculus, in: 10th International Conference on Non-Classical Logics, Theory and
Applications, NCL 2022, volume 358 of EPTCS, 2022, pp. 136–149.
[7] D. Larchey-Wendling, D. Méry, D. Galmiche, STRIP: Structural sharing for efficient proof-search,
in: First International Joint Conference on Automated Reasoning, IJCAR 2001, LNCS 2083, Siena,
Italy, 2001, pp. 696–700.
36
A. AutoPSI Session Capture
37