Introduction

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 difference 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 1. we further refine labelled sequent calculi for conditional logics in order to tackle question (ii) above. To this aim, we introduce SeqS 23 , 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 SeqS 23 : 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 SeqS 23 and compared them with those of the most recent version of CondLean [21], obtaining promising results that confirm that avoiding label substitution leads to a significant improvement of the performances of the prover.

Conditional Logics and the Selection Function Semantics

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.

Definition 1 (Syntax of Conditional Logics).

A propositional conditional language ℒ contains:

• a set of propositional variables ATM ;

• the constants ⊥ and ⊤;

• the set of connectives ¬ (unary), ∧, ∨, →, ⇒ (binary).

Formulas of ℒ are inductively defined as follows:

• 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:

Definition 2 (Selection function semantics). 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 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

-[⊥] = ∅ -[⊤] = 𝒲 -[¬𝐴] = 𝒲 ∖ [𝐴] -[𝐴 ∧ 𝐵] = [𝐴] ∩ [𝐵] -[𝐴 ∨ 𝐵] = [𝐴] ∪ [𝐵] -[𝐴 → 𝐵] = (𝒲 ∖ [𝐴]) ∪ [𝐵] -[𝐴 ⇒ 𝐵] = {𝑤 ∈ 𝒲 | 𝑓 (𝑤, [𝐴]) ⊆ [𝐵]} As usual,[𝐴] = [𝐴 ′ ] 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 = ⟨{𝑤, 𝑢, 𝑣}, 𝑓 We consider the following standard extensions of the basic system of Conditional Logics CK:

Logic Axiom Model condition ID 𝐴 ⇒ 𝐴 𝑓 (𝑤, [𝐴]) ⊆ [𝐴] CS (𝐴 ∧ 𝐵) → (𝐴 ⇒ 𝐵) 𝑤 ∈ [𝐴] → 𝑓 (𝑤, [𝐴]) ⊆ {𝑤} CEM (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ ¬𝐵) | 𝑓 (𝑤, [𝐴]) |≤ 1 MP (𝐴 ⇒ 𝐵) → (𝐴 → 𝐵) 𝑤 ∈ [𝐴] → 𝑤 ∈ 𝑓 (𝑤, [𝐴])

The above axiomatizations are complete with respect to the respective semantics [2]. We can observe that:

Sequent Calculi for Conditional Logics with Strong Centering

In this section we introduce SeqS 23 , 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

(𝑦) ∈ 𝑓 (𝐼(𝑥), [𝐴]). 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 SeqS 23 , 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 SeqS 23 , 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:

Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴 Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵 (CS) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵 replacing the following one, introduced in [17]: Γ, 𝑥 𝐴 −→ 𝑦 ⊢ Δ, 𝑥 : 𝐴 Γ[𝑥/𝑢, 𝑦/𝑢], 𝑢 𝐴 −→ 𝑢 ⊢ Δ[𝑥/𝑢, 𝑦/𝑢] (CS) Γ, 𝑥 𝐴 −→ 𝑦 ⊢ Δ

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:

(⇒ R) 𝑥 : 𝐴, 𝑥 : 𝐵, 𝑥 𝐴 −→ 𝑧, 𝑥 𝐴 −→ 𝑦 ⊢ 𝑧 : 𝐶, 𝑦 : 𝐵, 𝑥 : 𝐴 ⇒ 𝐷 (⇒ R) 𝑥 : 𝐴, 𝑥 : 𝐵, 𝑥 𝐴 −→ 𝑦 ⊢ 𝑦 : 𝐵, 𝑥 : 𝐴 ⇒ 𝐶, 𝑥 : 𝐴 ⇒ 𝐷 (⇒ R) 𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴 ⇒ 𝐶, 𝑥 : 𝐴 ⇒ 𝐷 (∨R) 𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷) (∨R) 𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷) (∧L) 𝑥 : 𝐴 ∧ 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)

whereas in the novel calculi SeqS 23 one can obtain the following, shorter derivation: 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:

Proposition 5. If Γ ⊢ Δ, 𝑥 𝐴 −→ 𝑦 is derivable in SeqS 23 in systems with the rule (CS), then either (i) Γ ⊢ Δ is derivable in SeqS 23 or (ii) 𝑥 = 𝑦 or (iii) there exists 𝑥 𝐴 ′ −→ 𝑦 ∈ Γ such that 𝑥 𝐴 ′ −→ 𝑦 ⊢ 𝑥 𝐴 −→ 𝑦 is derivable in SeqS 23 .

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 SeqS 23 , 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 23 , where Γ ′ is obtained by replacing in Γ any number of transition formulas

𝑥 𝐴 −→ 𝑦 with 𝑥 𝐴 ′ −→ 𝑦, where 𝐴 and 𝐴 ′ are equivalent 1 , is derivable too. For instance, if Γ, 𝑥 𝐴∨𝐵 −→ 𝑦, 𝑥 𝐴∨𝐵 −→ 𝑧 ⊢ Δ is derivable, so are the sequents Γ, 𝑥 𝐴∨𝐵 −→ 𝑦, 𝑥 ¬𝐴→𝐵 −→ 𝑧 ⊢ Δ and Γ, 𝑥 ¬𝐴→𝐵 −→ 𝑦, 𝑥 ¬𝐴→𝐵 −→ 𝑧 ⊢ Δ. Proposition 6. If 𝑥 𝐴 ′ −→ 𝑦 ⊢ 𝑥 𝐴 −→ 𝑦 and Γ ⊢ Δ are derivable in SeqS 23 , then Γ ′ ⊢ Δ is also derivable in in SeqS𝑥 𝐴 −→ 𝑦 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:

Theorem 7. The cut rule:

Γ ⊢ Δ, 𝐹 𝐹, Γ ⊢ Δ (𝑐𝑢𝑡) Γ ⊢ Δ

where 𝐹 is any labelled formula, is admissible in SeqS 23 , i.e. if Γ ⊢ Δ, 𝐹 and 𝐹, Γ ⊢ Δ are derivable in SeqS 23 , 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 (3) is derivable, so is (3 ′ ) Γ, 𝑥 : 𝐵 ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵. We can apply the inductive hypothesis on the sum of the heights of the derivations of the two premises to cut (3 ′ ) and (5), to obtain a derivation of (7) Γ, 𝑥 : 𝐵 ⊢ Δ. Similarly, since (6) is derivable, then so is (6 ′ ) Γ, 𝑥 : 𝐴 ⇒ 𝐵 ⊢ Δ, 𝑥 : 𝐵, and we can apply the inductive hypothesis on the sum of the heights to cut (6 ′ ) and (2) and obtain a proof of (8) Γ ⊢ Δ, 𝑥 : 𝐵. We can the conclude that Γ ⊢ Δ is derivable by applying the inductive hypothesis on the complexity of the cut formula to (7) and (8).

In case (iii), by Proposition 6 and the fact that also 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 SeqS 23 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:

𝑥 𝐴 −→ 𝑦 ⊢ 𝑥 𝐴 ′ −→ 𝑦 is derivable, we have that Γ ′ , 𝑥 𝐴 −→ 𝑦 ⊢ Δ is derivable, where Γ = Γ ′ , 𝑥 𝐴 ′ −→ 𝑦.(1) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴 (2) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵 (CS) (3) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵

By inductive hypothesis, the sequents (1) and (2) are valid. By absurd, suppose that (3) is not, that is to say there exists a model ℳ and a mapping 𝐼 satisfying all formulas in Γ but falsifying all formulas in the right-hand side of the sequent, namely all formulas in Δ and 𝑥 : 𝐴 ⇒ 𝐵. Concerning the latter, there exists a world 𝑤 such that (*) 𝑤 ∈ 𝑓 (𝐼(𝑥), [𝐴]) and (**) 𝑤 ̸ ∈ [𝐵]. By the validity of (1), we have that, since ℳ satisfies via 𝐼 all formulas in Γ, at least one formula in the right-hand side of the sequent must be satisfied by ℳ via 𝐼 too. Necessarily, we have that ℳ satisfies 𝑥 : 𝐴 (all formulas in Δ are falsified): this means that 𝐼(𝑥) ∈ [𝐴]. By the strong centering condition, it turns out that 𝑓 (𝐼(𝑥), [𝐴]) ⊆ {𝐼(𝑥)}. Given (*), we have that 𝐼(𝑥) = 𝑤. By the validity of (2), reasoning in the same way we have that

𝐼(𝑥) = 𝑤 ∈ [𝐵], contradicting (**).

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 SeqS 23 . 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].

The Theorem Prover CondLean 4.0

In this section we introduce CondLean 4.0, a Prolog implementation of the calculi SeqS 23 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 efficient first-order theorem prover, called leanT A P, consisting of only five Prolog clauses. The basic idea of the "lean" methodology is "to achieve maximal efficiency 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 SeqS 23 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 SeqS 23 , 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 SeqS 23 . 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): 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):

prove(Gamma,[LitDelta,TransDelta,ComplexDelta], Labels, RCond, LCond, CS, tree(cs,SubTree1,SubTree2)):- 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 𝑖𝑖𝑖).

member([X,A => B],ComplexDelta), ∖+member([X,A => B],CS),!,(𝑖𝑖𝑖)

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.

Performance of CondLean 4.0

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 inefficient 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.

Conclusions, Related Works, Future Issues

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 inefficient 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 efficient 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.