In this work we continue our investigation on proof methods and theorem proving for Conditional Logics with the selection function semantics. Conditional Logics recently have received a renewed attention and have found several applications in knowledge representation and artificial intelligence. We present a labelled sequent calculus for systems including the axiom of strong centering CS, as well as a theorem prover implementing the sequent calculus in Prolog.
Conditional Logics have a long history, starting with the seminal works [1, 2, 3, 4, 5] in the seventies. In the last decades, Conditional Logics have found a renewed interest in several fields of artificial intelligence and knowledge representation, from hypothetical reasoning to belief revision, from diagnosis to nonmonotonic reasoning and planning [6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16].
Conditional Logics are extensions of classical logic by a binary operator ⇒, called conditional operator, used in order to express formulas of the form ⇒ . Similarly to modal logics, the semantics of Conditional Logics can be defined in terms of possible world structures. In this respect, Conditional Logics can be seen as a generalization of modal logics (or a type of multi-modal logic) where the conditional operator is a sort of modality indexed by a formula of the same language. However, as a diference with modal logics, the lack of a universally accepted semantics led to a partial underdevelopment of proof methods and theorem provers for these logics.
An attempt to fill this gap has been proposed in [ 17], where labelled sequent calculi for conditional logics with the selection function semantics ([2]) are introduced. Intuitively, the selection function selects, for a world and a formula , the set of worlds (, ) which are “most-similar to " given the information . In normal conditional logics, depends on the set of worlds satisfying rather than on itself, so that (, ) = (, ′) whenever and ′ are true in the same worlds. A conditional formula ⇒ is true in whenever is true in every world selected by for and . Since we adopt the selection function semantics, CK is the fundamental system, it has the same role as the system K (from which it derives its name) in modal logic. Formulas valid in CK are exactly those ones that are valid in every selection function model. Extensions are then obtained by imposing restrictions on the selection function. In [17], CK and some standard extensions with conditions ID (conditional identity), MP (conditional modus ponens), CEM (conditional third excluded middle), and CS (conditional strong centering), as well as most of the combinations of them are investigated. The proposed calculi, called SeqS, are modular, in some cases optimal and have been implemented by several versions of a “lean” style Prolog program called CondLean [18, 19, 20].
The original SeqS calculi, as well as their implementation CondLean, have two main drawbacks: (i) they neglect all the systems including both the axioms CEM and MP: the reason is that the proof of cut elimination, needed in order to prove the completeness of the calculi, does not work when such axioms are considered together; (ii) the rules dealing with the conditions CS and CEM are based on a label substitution mechanism that leads to a very ineficient implementation. A solution to (i) has been provided in [20, 21], where calculi for the whole cube of the extensions of CK generated by the above axioms are proposed, including those with both CEM and MP. The theorem prover implementing these calculi has better performance than CondLean, however, the problem (ii) is far from being solved: indeed, the rule for CS is still based on the label substitution mechanism, and the performances of the theorem prover are just increased in systems with both MP and CEM where the rule for CS can be omitted since the axiom (CS) is derivable (see Proposition 3). The relevance of strong centering is motivated by the concept of similarity: if holds in a world , then the -world which is more similar to is itself. Moreover, strong centering is needed in order to perform inferences that are plausible in several contexts, such as if ⇒ holds and holds, then also holds (a kind of conditional modus ponens), as well as the principle that a subjunctive conditional is false if its antecedent is true and its consequent is false, namely if ∧ ¬ holds, then so is ¬( ⇒ ).
In this work we try to provide a final solution to the problem of eficient theorem proving for Conditional Logics with selection function semantics. We can identify two main contributions of this work: 1. we further refine labelled sequent calculi for conditional logics in order to tackle question (ii) above. To this aim, we introduce SeqS23, labelled sequent calculi for CK and the whole cube of the combinations of extensions with axioms CS, CEM, MP, and ID, where also the rule for CS does no longer exploit label substitutions. We show that one can derive a decision procedure from the cut-free calculi, providing a constructive proof of decidability of the logics considered. By estimating the size of the finite derivations of a given sequent, we also obtain a polynomial space complexity bound for these logics; 2. we introduce CondLean 4.0, a Prolog implementation of the proposed calculi SeqS23: the program is inspired by the “lean” methodology, whose aim is to write short programs and exploit the power of Prolog’s engine as much as possible: in this respect, every clause of a single predicate, called prove, implements an axiom or rule of the calculi and the proof search is provided for free by the mere depth-first search mechanism of Prolog, without any additional ad hoc mechanism. We have tested the performances of SeqS23 and compared them with those of the most recent version of CondLean [21], obtaining promising results that conrfim that avoiding label substitution leads to a significant improvement of the performances of the prover.
In this section we recall Conditional Logics. We first define the language and the syntax of Conditional Logics, then we present the semantics based on a selection function. Last, we provide an axiomatization of the systems of Conditional Logics we consider.
tains:
• a set of propositional variables ATM ; • the constants ⊥ and ⊤; • the set of connectives ¬ (unary), ∧, ∨, →, ⇒ (binary).
• atomic formulas ∈ ATM , ⊥ and ⊤ are formulas of ℒ; • given and formulas of ℒ, complex formulas ¬, ∧ , ∨ , → , and ⇒ are formulas of ℒ.
Let us now introduce the selection function semantics [2]. Intuitively, a conditional formula ⇒ holds in a possible world if holds in all the worlds that are most similar to given the information . Such worlds are those selected by the selection function for and .
We define the selection function semantics as follows:
A model is a triple ℳ = ⟨, , [ ]⟩ where: • is a non-empty set of worlds; • is the selection function : × 2 →− 2 • [ ] is the evaluation function, which assigns to an atom ∈ ATM the set of worlds where is true, and is extended to complex formulas as follows: – [⊥] = ∅ – [⊤] = – [¬] = ∖ [] – [ ∧ ] = [] ∩ [] – [ ∨ ] = [] ∪ [] – [ → ] = ( ∖ []) ∪ [] – [ ⇒ ] = { ∈ | (, []) ⊆ []} As usual, a formula is valid in a model ℳ, written ℳ |= , if it holds in all the worlds of ℳ, i.e. ℳ |= if and only if [ ] = . A formula is valid, written |= , if it is valid in all models, i.e. |= if and only if ℳ |= for all ℳ.
As mentioned above, the selection function selects, for a world and a formula , the set of worlds of which are closer/similar to given the information . A conditional formula ⇒ holds in a world if the formula holds in all the worlds selected by for and . It is worth noticing that we have defined taking [] rather than (i.e. (, []) rather than (, )) as an argument; this is equivalent to define on formulas, i.e. (, ) but imposing that if [] = [′ ] in the model, then (, ) = (, ′ ). This condition is called normality.
The semantics above characterizes the basic conditional logic CK. Formulas that are valid in CK are valid in all selection function models.
An axiomatization of this system is given by: • any axiomatization of classical propositional calculus; • (Modus Ponens) • (RCEA) • (RCK) → → → ( ⇒ ) ↔ ( ⇒ ) (1 ∧ · · · ∧
) → ( ⇒ 1 ∧ · · · ∧
⇒ ) → ( ⇒ ) As for modal logics, in order to perform useful inferences, we can consider extensions of CK by assuming further properties on the selection function. Let us consider, for instance, the conditional third excluded middle, namely the formula
( ⇒ ) ∨ ( ⇒ ¬) This formula is not valid: as an example, consider the model ℳ1 = ⟨{, , }, 1, [ ]1⟩, where the selection function 1 is such that 1(, []) = {, } and the evaluation is []1 = {}. We have that ℳ1 ̸|= ( ⇒ ) ∨ ( ⇒ ¬). Indeed, ̸∈ [( ⇒ ) ∨ ( ⇒ ¬)], since neither ∈ [ ⇒ ] nor ∈ [ ⇒ ¬]. ⇒ does not hold in , since there exists , which is similar to given (selected by 1 for and ) where does not hold ( holds only in ). Similarly, ⇒ ¬ does not hold in , since there exists , which is similar to given (selected by 1 for and ) where holds. Such a formula is however valid if we restrict our concern to models where the selection function can select at most one world, that is to say imposing the condition: | (, []) | ≤ 1 Obviously, the above counter model ℳ1 cannot be considered, in other words either or can be the only world selected by for and , then either ⇒ or ⇒ ¬ holds in .
We consider the following standard extensions of the basic system of Conditional Logics CK:
⇒ ( ∧ ) → ( ⇒ ) ( ⇒ ) ∨ ( ⇒ ¬) ( ⇒ ) → ( → )
(, []) ⊆ [] ∈ [] → (, []) ⊆ { } | (, []) |≤ 1 ∈ [] → ∈ (, []) The above axiomatizations are complete with respect to the respective semantics [2]. We can observe that: Proposition 3. In systems with both axioms (CEM) and (MP), axiom (CS) is derivable. Indeed, for (CEM) we have that | (, []) |≤ 1. For (MP), we have that, if ∈ [], then ∈ (, []). Therefore, it follows that if ∈ [], then (, []) = {}, satisfying the (CS) condition.
In this section we introduce SeqS23, a family of labelled sequent calculi for the conditional systems under consideration. The calculi are modular and they are able to deal with the basic system CK as well as with the whole cube of extensions with axioms ID, CS, CEM and MP.
The calculi make use of labels to represent possible worlds. We consider a language ℒ and a denumerable alphabet of labels , whose elements are denoted by x, y, z, .... There are two kinds of labelled formulas: world formulas, denoted by x: A, where x ∈ and ∈ ℒ, used to represent that A holds in a world x; transition formulas, denoted by x →− y, where x, y ∈ and ∈ ℒ. A transition formula x →− y represents that y ∈ f (x, [A]).
A sequent is a pair ⟨Γ, Δ⟩, usually denoted with Γ ⊢ Δ, where Γ and Δ are multisets of labelled formulas. The intuitive meaning of Γ ⊢ Δ is: every model that satisfies all labelled formulas of Γ in the respective worlds (specified by the labels) satisfies at least one of the labelled formulas of Δ (in those worlds).
Formally: G Definition 4 (Validity of a sequent). Given a model ℳ = ⟨, , [ ]⟩ for ℒ, and a label alphabet , we consider any mapping : → . Let be a labelled formula, we define ℳ |= as ℳ |= : if and only if () ∈ [] and ℳ |= →− if and only if () ∈ ((), []).
We say that Γ ⊢ Δ is valid in ℳ if for every mapping : → , if ℳ |= for every ∈ Γ, then ℳ |= for some ∈ Δ.
We say that Γ ⊢ Δ is valid in a system (CK or any extension of it) if it is valid in every ℳ satisfying the specific conditions for that system.
We say that a sequent Γ ⊢ Δ is derivable if it admits a derivation in SeqS23, i.e. a proof tree, obtained by applying backwards the rules of the calculi, having Γ ⊢ Δ as a root and whose leaves are all instances of closing rules, i.e. rules with valid sequents called (). As usual, the idea is as follows: in order to prove that a formula is valid in a conditional logic, then one has to check whether the sequent ⊢ : is derivable in SeqS23, i.e. if we can obtain a proof tree by applying backwards the rules, starting from the root ⊢ : .
The novelty with respect to the calculi introduced in [17] and [20] is the following invertible rule for CS, no longer exploiting a label substitution, whose principal formula is a conditional : ⇒ on the right-hand side of the sequent: Γ ⊢ Δ, : ⇒ , :
Γ ⊢ Δ, : ⇒ , : Γ ⊢ Δ, : ⇒ replacing the following one, introduced in [17]: Γ, →− ⊢ Δ, :
Γ[/, /], →− ⊢ Δ[/, /] Γ, →− ⊢ Δ where Γ[/, /] (respectively, Δ[/, /]) is obtained from Γ (respectively, from Δ) by replacing every occurrence of and with a new label .
The basic idea is as follows: when a conditional : ⇒ belongs to the right-hand side of a sequent, this means that there exists a world selected by for the world represented by and such that does not hold in . By the strong centering condition, if the world represented by is an world (left premise), then is necessarily the world itself, then does not hold in it, therefore : is added in the right-hand side of the sequent of the right premise.
As an example, consider the following valid sequent in systems with axiom (CS): : ∧ ⊢ : ( ⇒ ) ∨ ( ⇒ ) ∨ ( ⇒ ) In the calculi SeqS, the derivation could be as follows: (CS) (CS) whereas in the novel calculi SeqS23 one can obtain the following, shorter derivation: () : ⊢ :
: , . . . , →− ⊢ : , : , : : , : , →− , →− , →− ⊢ : , : , : (CS) (CS) : ⊢ : : , : , →− , →− , →− ⊢ : , : , : (CS) : , : , →− , →− , →− ⊢ : , : , : : , : , →− , →− ⊢ : , : , : ⇒ : , : , →− ⊢ : , : ⇒ , : ⇒ : , : ⊢ : ⇒ , : ⇒ , : ⇒ : , : ⊢ : ⇒ , : ( ⇒ ) ∨ ( ⇒ ) : , : ⊢ : ( ⇒ ) ∨ ( ⇒ ) ∨ ( ⇒ ) : ∧ ⊢ : ( ⇒ ) ∨ ( ⇒ ) ∨ ( ⇒ ) (⇒ R) (⇒ R) (⇒ R) (∨R) (∨R) (∧L)
The calculi SeqS23 are shown in Figure 1. They satisfy basic structural properties, namely : , : ⊢ : ⇒ , : : , : ⊢ : ⇒ , : (CS) : , : ⊢ : ⇒ : ∧ ⊢ : ⇒ ⊢ : ( ∧ ) → ( ⇒ ) (∧L) (→ R) height-preserving admissibility of weakening, height-preserving invertibility of the rules (with the exception of (EQ)), height-preserving admissibility of contraction.
Moreover, the following properties are needed in order to prove the admissibility of the cut rule (see Theorem 7 below), in turn needed to prove the completeness of the calculi: →−′ ⊢ →− is derivable in SeqS23.
Proposition 5. If Γ ⊢ Δ, →− is derivable in SeqS23 in systems with the rule (CS), then either (i) Γ ⊢ Δ is derivable in SeqS23 or (ii) = or (iii) there exists →−′ ∈ Γ such that Proof. (sketch) By induction on the height of the derivation of Γ ⊢ Δ, →− . Intuitively, if the transition formula →− is used in the derivation, then either it is the principal formula in a backward application of (MP), then it must be = and () holds, otherwise it is the principal formula in a backward application of (EQ), therefore there exists another transition formula →−′ ∈ Γ such that →−′ ⊢ →− is derivable in SeqS23, thus () holds. On the contrary, if →− is not used in the derivation, then we have that also Γ ⊢ Δ is derivable, thus () holds. ■ The following proposition states that, given a derivable sequent Γ ⊢ Δ, the sequent obtained by replacing in Γ and/or Δ one or more transition formulas →− with →−′ , where and ′ are equivalent1, is derivable too. For instance, if Γ, →− ∨ ⊢ Δ is derivable, ∨ , →− ∨ , ¬→−→ ⊢ Δ and Γ, ¬→−→ , ¬→−→ ⊢ Δ. so are the sequents Γ, →− Proposition 6. If →−′ ⊢ →− and Γ ⊢ Δ are derivable in SeqS23, then Γ′ ⊢ Δ is also derivable in in SeqS23, where Γ′ is obtained by replacing in Γ any number of transition formulas →− with →−′ .
The proof is by induction on the height of the derivation of Γ ⊢ Δ, is straightforward, therefore left to the reader in order to save space.
As mentioned, we can show that the following cut rule is admissible: 1As usual, this means that both → ′ and ′ → are valid.
Theorem 7. The cut rule: Γ ⊢ Δ, , Γ ⊢ Δ
() Γ ⊢ Δ where is any labelled formula, is admissible in SeqS23, i.e. if Γ ⊢ Δ, and , Γ ⊢ Δ are derivable in SeqS23 , so is Γ ⊢ Δ.
Proof. We proceed in the standard way by a double induction over the complexity of the cut formula and the sum of the heights of the derivations of the two premises of cut, namely we replace one cut by one or several cuts on formulas of smaller complexity, or on sequents derived by shorter derivations. To save space, we show the most interesting case involving the novel rule (CS) and we left the other cases to the reader. Consider the case in which the proof is ended as follows: Γ ⊢ Δ, : ⇒ , : Γ ⊢ Δ, : ⇒ , : (* ) Γ ⊢ Δ, : ⇒ (CS) (* ) Γ, : ⇒ ⊢ Δ, →− Γ, : ⇒ , : ⊢ Δ Γ, : ⇒ ⊢ Δ ()
(⇒ )
Γ ⊢ Δ
Since weakening is admissible and the fact that (* ) is derivable, we have that also (♣) Γ ⊢
Δ, : ⇒ , →− is derivable. We can apply the inductive hypothesis on the sum of
the heights to cut (♣) and (* ) to obtain a derivation of (♠ ) Γ ⊢ Δ, →− . By Proposition 5
we have that either (i) Γ ⊢ Δ is derivable, and we are done, or (ii) = , or (iii) there exists
→−′ ∈ Γ such that →−′ ⊢ →− is derivable. In case (ii), the proof is ended as follows:
(
(⇒ ) ()
Since weakening is height-preserving admissible, since (
In case (iii), by Proposition 6 and the fact that also →− ⊢ →−′ is derivable, we have that Γ′, →− ⊢ Δ is derivable, where Γ = Γ′, →−′ . By applying the inductive hypothesis Theorem 8 (Soundness and completeness). Given a conditional formula , it is valid in a conditional logic if and only if it is derivable in the corresponding calculus of SeqS23, that is to say |= if and only if ⊢ : is derivable in SeqS23.
Proof. Concerning the soundness, we have to prove that, if a sequent Γ ⊢ Δ is derivable, then
the sequent is valid. This can be done by induction on the height of the derivation of Γ ⊢ Δ.
The basic cases are those corresponding to derivations of height 0, that is to say instances of
(). It is easy to see that, in all these cases, Γ ⊢ Δ is a valid sequent. As an example, consider
Γ, : ⊢ Δ, : : consider every model ℳ and every mapping satisfying all formulas in
the left-hand side of the sequent, then also : . This means that () ∈ [ ], but then we
have that ℳ satisfies via at least a formula in the right-hand side of the sequent, the same
: . For the inductive step, we proceed by considering each rule of the calculi SeqS23 in order
to check that, if the premise(s) is (are) valid sequent(s), to which we can apply the inductive
hypothesis, so is the conclusion. To save space, we only present the case of the novel (CS), the
other ones are left to the reader. Let us consider a derivation ended as follows:
(
(
By inductive hypothesis, the sequents (
The completeness is an easy consequence of the admissibility of the cut rule (Theorem 7): by induction on the complexity of the formulas we can prove that, if a formula is valid in a conditional logic, then ⊢ : is derivable in SeqS23. It can be shown that axioms are derivable and that the set of derivable formulas is closed under (Modus Ponens), (RCEA), and (RCK). A derivation of (CS) is provided in Figure 2. For the other axioms and rules, we remind the reader to [17, 20] in order to save space.
The presence of labels and of the rules (⇒ L), (⇒ R), (ID), (MP), (CEM), and (CS), which increase the complexity of the sequent in a backward proof search, is a potential cause of a non-terminating proof search. However, with a similar argument to the one proposed in [17], we can define a procedure that can apply such rules in a controlled way and introducing a finite number of labels, ensuring termination. Intuitively, it can be shown that it is useless to apply (⇒ L) and (⇒ R) on : ⇒ by introducing (looking backward) the same transition formula →− more than once in each branch of a proof tree. Similarly, it is useless to apply (ID), (MP), (CEM), and (CS) on the same formula more than once in a backward proof search on each branch of a derivation. This leads to the decidability of the given logics: Theorem 9 (Decidability). Conditional Logics CK and all its extensions with axioms ID, MP, CS, CEM and all their combinations are decidable.
It can be shown that provability in all the Conditional Logics considered is decidable in (2 log ) space, we omit the proof which is essentially the same as in [17].
In this section we introduce CondLean 4.0, a Prolog implementation of the calculi SeqS23 introduced in the previous section. As already mentioned, the prover improves the existing provers for that logics [19, 18, 21] and is inspired to the “lean” methodology, introduced by Beckert and Posegga in the middle of the 90s [22, 23, 24]: they have proposed a very elegant and extremely eficient first-order theorem prover, called leanTAP, consisting of only five Prolog clauses. The basic idea of the “lean” methodology is “to achieve maximal eficiency from minimal means” [22] by writing short programs and exploiting the power of Prolog’s engine as much as possible. Moreover, it is straightforward to prove soundness and completeness of the theorem prover by exploiting the one to one correspondence between axioms/rules of SeqS23 and clauses of CondLean 4.0.
Let us now describe the theorem prover CondLean 4.0 in detail.
Each component of a sequent is implemented by a list of formulas, partitioned into three sub-lists: atomic formulas, transitions and complex formulas. Atomic and complex formulas are implemented by a Prolog list of the form [x,a], where x is a Prolog constant and a is a formula. A transition formula x →− y is implemented by a Prolog list of the form [x,a,y]. Labels are implemented by Prolog constants. The sequent calculi are implemented by the predicate prove(Gamma, Delta, Labels, Rcond, LCond, Tree) which succeeds if and only if Γ ⊢ Δ is derivable in SeqS23, where Gamma and Delta are the lists implementing the multisets Γ and Δ, respectively, and Labels is the list of labels introduced in that branch. Each clause of the prove predicate implements one axiom or rule of SeqS23. Further arguments RCond and LCond are used in order to ensure the termination of the proof search, essentially by restricting the application of rules (⇒ L) and (⇒ R), copying their principal formulas in both the premises (more details are provided here below). Tree is an output term: if the proof search succeeds, it matches a Prolog representation of the derivation found by the theorem prover.
The theorem prover proceeds as follows. First of all, if Γ ⊢ Δ is an axiom, then the goal will succeed immediately by using the clauses for the axioms. If it is not, then the first applicable rule is chosen. The ordering of the clauses is such that the application of the branching rules is postponed as much as possible. Concerning the interplay among the rules dealing with conditional formulas on the right-hand side of a sequent, the new rule (CS) rule is applied first: intuitively, this is needed in order to check whether the conditional formula under consideration can be handled by the current world itself, otherwise the rule (⇒ R), which introduces a new label in a backward proof search, it is first applied and, if this does not lead to a derivation, the rule (CEM) – if available – is applied.
As mentioned here above, arguments RCond and LCond are used in order to ensure the termination of the proof search by controlling the application of the rules (⇒ L) and (⇒ R): indeed, these rules copy the conditional formula : ⇒ to which they are applied in their premises, therefore we need to avoid redundant applications that, otherwise, would lead to expand an infinite branch. As an example, RCond is a Prolog list containing all the formulas : ⇒ to which the rule (⇒ R) has been already applied on the current branch: such a rule will be then applied to : ⇒ only if it does not belong to the list RCond. A similar mechanism is implemented for extensions of CK, namely further suitable arguments are added to the predicate prove to keep track of the information needed to avoid useless and uncontrolled applications of the rules (MP), (ID), (CEM), and (CS), which copy their principal formulas in their premise(s).
Let us now present some clauses of CondLean 4.0. As a first example, the clause for the axiom checking whether the same atomic formula occurs in both the left and the right hand side of a sequent is implemented as follows: prove([LitGamma,_,_],[LitDelta,_,_],_,_,_,tree(ax)):
member(F,LitGamma),member(F,LitDelta),!.
It is easy to observe that the rule succeeds when the same labelled formula belongs to both the right and the left hand side of the sequent under investigation, completing the proof search: indeed, no recursive call to the predicate prove is performed, and the output term Tree matches a representation of a leaf in the derivation (tree(ax)).
As another example, here is the clause implementing (⇒ L): prove([LitGamma,TransGamma,ComplexGamma],[LitDelta,TransDelta,ComplexDelta],
Labels, RCond, LCond, CS, tree(condL,SubTree1,SubTree2)):member([X,A => B],ComplexGamma), select([[X,A => B],Used],Cond,TempCond), member(Y,Labels), () ∖+member([Y,[X,A => B]],LCond),!, () put([Y,B],LitGamma,ComplexGamma,NewLitGamma,NewComplexGamma), prove([[[X, A => B],[[X,C,Y] | Used]] | TempCond], [LitGamma,TransGamma,ComplexGamma], [LitDelta,[[X,A,Y]|TransDelta],ComplexDelta],Labels), prove([[[X, A => B],[[X,C,Y] | Used]] | TempCond], [NewLitGamma,TransGamma,NewComplexGamma], [LitDelta,TransDelta,ComplexDelta],Labels).
The predicate put is used to put the labelled formula [Y,A] in the proper sub-list of the lefthand side of the sequent. The recursive calls to prove implement the proof search on the two premises. The output term Tree matches a Prolog term tree(condL,SubTree1,SubTree2), representing a tree with two branches, corresponding to the subtrees of the two premises SubTree1 and SubTree2 obtained by an application of the rule condL.
As mentioned, in order to ensure termination, in lines and the theorem prover checks whether (⇒ L) has been already applied on the current branch to the conditional formula : ⇒ by using the label , in other words by introducing →− and : in the premises. This avoids useless applications of the rule, by adopting the same label.
Let us now show the code of the novel rule (CS):
Also for this rule, in order to ensure termination, the theorem prover checks whether (CS) has been already applied on the current branch to the conditional formula : ⇒ , in order to avoid further – useless – applications (line ).
In order to search a derivation of a sequent Γ ⊢ Δ, the theorem prover proceeds as follows. First, if Γ ⊢ Δ is an axiom, the goal will succeed immediately by using the clauses for the axioms. If it is not, then the first applicable rule is chosen, e.g. if ComplexGamma contains a formula [X,A and B], then the clause implementing the rule (∧ L) is applied, invoking prove on its unique premise. The prover proceeds in a similar way for the other rules. As already mentioned, the ordering of the clauses is such that the application of the branching rules is postponed as much as possible.
In order to check whether a formula is valid in one of the considered systems, one has just to invoke the following auxiliary predicate:
pr(Formula) or pr(Formula,ProofTree) which wraps the prove predicate by a suitable initialization of its arguments. ()
We have tested CondLean 4.0 and we have compared its performance with those of the last version of CondLean [21]. We have tested the theorem prover over both: • a set of valid formulas • a set of randomly generated formulas, either valid or not.
We have observed that, over valid formulas, the performances of CondLean 4.0 are improved of 12, 35% with respect to its predecessor. As an example, running both the provers over the formula
( ∧ 1 ∧ 2 ∧ . . . ∧ 50) → (( ⇒ 1) ∨ ( ⇒ 2) ∨ . . . ∨ ( ⇒ 50)) CondLean 4.0 is able to build a derivation in 27 ms, against the 567 ms needed by the prover adopting label substitution.
Over randomly generated formulas, the statistics are even better: CondLean 4.0 provides an improvement of the performances of about 35%. We can then observe that its performance are promising, especially concerning cases in which it has to provide a negative answer for a not valid formula: this is justified by the fact that the previous implementations have to spend a lot of time in computing the ineficient label substitution mechanism, needed to succeed.
CondLean 4.0 is available for free download at https://gitlab2.educ.di.unito.it/pozzato/ condlean-4.0.git, where one can also find Prolog source files used in order to evaluate the performances described in this section.
In this work we have introduced CondLean 4.0, a theorem prover for Conditional Logics implementing labelled sequent calculi for the basic system CK and the whole cube of extensions with well established axioms ID, MP, CEM, and CS. Concerning the last one, known as conditional strong centering, the calculi considered are new, obtained from existing calculi [20] by replacing a rule computing a label substitution with a standard one, and are of their own interest. The performances of CondLean 4.0 seem promising and are better than those of its predecessors [19, 18, 21]: this is quite obvious if we consider that, in the most recent version of the prover, condition (CS) is handled either by a complicated and ineficient label substitution or by the combination of the rules for (CEM) and (MP) in systems allowing both of them, since in these logics (CS) is derivable (Proposition 3). Such better performances witness that avoiding label substitution is a concrete step towards eficient theorem proving for Conditional Logics.
Concerning related works, we mention [17], where combinations of the conditional third excluded middle (CEM) and conditional modus ponens (MP) are neglected, and [25], where strong centering (CS) is replaced by the condition (CSO).
We plan to extend our work in several directions. First, we aim at extending the calculi and the implementation to stronger Conditional Logics. Moreover, we aim at extending the prover by adopting standard refinements, state of the art heuristics, and data structures, as well as by a graphical web interface for it. We also aim at extending the set of formulas adopted in the performance evaluation, in order to provide a more detailed and structured comparison, for instance parametrizing statistics with respect to the level of nesting of the conditional operator ⇒ in formulas. Last, we are currently working on an extension of CondLean 4.0 which is able to show a countermodel in case of a failed proof: in a XAI perspective, it is obviously crucial to provide a derivation showing that a formula/a sequent is valid as our prover currently does, however it is also important to show a counterexample when this is not the case. [17] N. Olivetti, G. L. Pozzato, C. B. Schwind, A Sequent Calculus and a Theorem Prover for
Standard Conditional Logics, ACM Transactions on Computational Logics (ToCL) 8 (2007). [18] N. Olivetti, G. L. Pozzato, Condlean: A theorem prover for conditional logics, in: M. C. Mayer, F. Pirri (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2003, Rome, Italy, September 9-12, 2003. Proceedings, volume 2796 of Lecture Notes in Computer Science, Springer, 2003, pp. 264–270. URL: https://doi.org/10.1007/978-3-540-45206-5_23. doi:10.1007/ 978-3-540-45206-5\_23. [19] N. Olivetti, G. L. Pozzato, Condlean 3.0: Improving condlean for stronger conditional logics, in: B. Beckert (Ed.), Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005, Proceedings, volume 3702 of Lecture Notes in Computer Science, Springer, 2005, pp. 328–332. URL: https://doi.org/10.1007/11554554_27. doi:10.1007/11554554\_27. [20] N. Panic, G. L. Pozzato, Eficient theorem proving for conditional logics with conditional excluded middle, in: R. Calegari, G. Ciatto, A. Omicini (Eds.), Proceedings of the 37th Italian Conference on Computational Logic, Bologna, Italy, June 29 - July 1, 2022, volume 3204 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 217–231. URL: http://ceur-ws. org/Vol-3204/paper_22.pdf. [21] N. Olivetti, N. Panic, G. L. Pozzato, Labelled sequent calculi for conditional logics: Conditional excluded middle and conditional modus ponens finally together, in: A. Dovier, A. Montanari, A. Orlandini (Eds.), AIxIA 2022 - Advances in Artificial Intelligence - XXIst International Conference of the Italian Association for Artificial Intelligence, AIxIA 2022, Udine, Italy, November 28 - December 2, 2022, Proceedings, volume 13796 of Lecture Notes in Computer Science, Springer, 2022, pp. 345–357. URL: https://doi.org/10.1007/ 978-3-031-27181-6_24. doi:10.1007/978-3-031-27181-6\_24. [22] B. Beckert, J. Posegga, leantap: Lean tableau-based deduction, Journal of Automated
Reasoning 15 (1995) 339–358. [23] B. Beckert, J. Posegga, Logic programming as a basis for lean automated deduction.,
Journal of Logic Programming 28 (1996) 231–236. [24] M. Fitting, leantap revisited, Journal of Logic and Computation 8 (1998) 33–47. [25] R. Alenda, N. Olivetti, G. L. Pozzato, Nested sequent calculi for normal conditional logics, Journal of Logic and Computation 26 (2016) 7–50. doi:10.1093/logcom/ext034.