=Paper=
{{Paper
|id=Vol-3428/paper16
|storemode=property
|title=Proof Methods and Theorem Proving for Conditional Logics with Strong Centering
|pdfUrl=https://ceur-ws.org/Vol-3428/paper16.pdf
|volume=Vol-3428
|authors=Valentina Gliozzi,Gian Luca Pozzato,Alberto Valese
|dblpUrl=https://dblp.org/rec/conf/cilc/GliozziPV23
}}
==Proof Methods and Theorem Proving for Conditional Logics with Strong Centering==
<pdf width="1500px">https://ceur-ws.org/Vol-3428/paper16.pdf</pdf>
<pre>
Proof Methods and Theorem Proving for Conditional
Logics with Strong Centering
Valentina Gliozzi1 , Gian Luca Pozzato1,* and Alberto Valese1
1
    Dipartimento di Informatica, Università degli Studi di Torino, 10149, Turin, Italy


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

                                         Keywords
                                         Conditional logics, Sequent calculi, Proof methods, Prolog, Nonmonotonic reasoning, Theorem proving




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

CILC’23: 38th Italian Conference on Computational Logic, June 21–23, 2023, Udine, Italy
*
 Corresponding author.
$ valentina.gliozzi@unito.it (V. Gliozzi); gianluca.pozzato@unito.it (G. L. Pozzato); alberto.valese@edu.unito.it
(A. Valese)
€ https://www.di.unito.it/~gliozzi (V. Gliozzi); https://www.di.unito.it/~pozzato (G. L. Pozzato);
https://www.di.unito.it/~valese (A. Valese)
 0000-0003-1045-8018 (V. Gliozzi); 0000-0002-3952-4624 (G. L. Pozzato)
                                       © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
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 draw-
backs: (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 inefficient imple-
mentation. 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 efficient 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 confirm that avoiding label substitution leads to a significant
      improvement of the performances of the prover.


2. 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 ℒ con-
tains:

    • 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 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)
                  (𝐴 ⇒ 𝐶) ↔ (𝐵 ⇒ 𝐶)
                           (𝐴1 ∧ · · · ∧ 𝐴𝑛 ) → 𝐵
    • (RCK)
                (𝐶 ⇒ 𝐴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:
  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:

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.


3. Sequent Calculi for Conditional Logics with Strong Centering
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 al-
phabet 𝒜, 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:

            Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴                             Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵
                                                                                               (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:
                                                              (𝐴𝑋)                        𝐴
                                                                                                                      (𝐴𝑋)
                                                𝑣:𝐴⊢𝑣:𝐴                 𝑤 : 𝐵, . . . , 𝑤 −→ 𝑤 ⊢ 𝑤 : 𝐶, 𝑤 : 𝐵, 𝑤 : 𝐷
                                    (𝐴𝑋)                            𝐴         𝐴          𝐴
                                                                                                                      (CS)
                     𝑢:𝐴⊢𝑢:𝐴                        𝑣 : 𝐴, 𝑣 : 𝐵, 𝑣 −→ 𝑣, 𝑣 −→ 𝑣, 𝑣 −→ 𝑦 ⊢ 𝑣 : 𝐶, 𝑦 : 𝐵, 𝑣 : 𝐷
            (𝐴𝑋)                                       𝐴        𝐴         𝐴
                                                                                                                 (CS)
𝑥:𝐴⊢𝑥:𝐴                            𝑢 : 𝐴, 𝑢 : 𝐵, 𝑢 −→ 𝑢, 𝑢 −→ 𝑧, 𝑢 −→ 𝑦 ⊢ 𝑧 : 𝐶, 𝑦 : 𝐵, 𝑢 : 𝐷
                               𝐴            𝐴            𝐴
                                                                                                    (CS)
               𝑥 : 𝐴, 𝑥 : 𝐵, 𝑥 −→ 𝑤, 𝑥 −→ 𝑧, 𝑥 −→ 𝑦 ⊢ 𝑧 : 𝐶, 𝑦 : 𝐵, 𝑤 : 𝐷
                                   𝐴            𝐴
                                                                                     (⇒ R)
                  𝑥 : 𝐴, 𝑥 : 𝐵, 𝑥 −→ 𝑧, 𝑥 −→ 𝑦 ⊢ 𝑧 : 𝐶, 𝑦 : 𝐵, 𝑥 : 𝐴 ⇒ 𝐷
                                       𝐴
                                                                                   (⇒ R)
                   𝑥 : 𝐴, 𝑥 : 𝐵, 𝑥 −→ 𝑦 ⊢ 𝑦 : 𝐵, 𝑥 : 𝐴 ⇒ 𝐶, 𝑥 : 𝐴 ⇒ 𝐷
                                                                                  (⇒ R)
                     𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴 ⇒ 𝐶, 𝑥 : 𝐴 ⇒ 𝐷
                                                                                  (∨R)
                    𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)
                                                                                  (∨R)
                    𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)
                                                                                  (∧L)
                    𝑥 : 𝐴 ∧ 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)

whereas in the novel calculi SeqS23 one can obtain the following, shorter derivation:
                                                  (𝐴𝑋)                                 (𝐴𝑋)
                    𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴, . . .          𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐵, . . .
                                                                                       (CS)
                         𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴 ⇒ 𝐶, 𝑥 : 𝐴 ⇒ 𝐷
                                                                                (∨R)
                        𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)
                                                                                (∨R)
                        𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)
                                                                                (∧L)
                         𝑥 : 𝐴 ∧ 𝐵 ⊢ 𝑥 : (𝐴 ⇒ 𝐵) ∨ (𝐴 ⇒ 𝐶) ∨ (𝐴 ⇒ 𝐷)




Figure 1: Rules of sequent calculi SeqS23
                                                                                              .

  The calculi SeqS23 are shown in Figure 1. They satisfy basic structural properties, namely
                                                  (𝐴𝑋)                                         (𝐴𝑋)
              𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴                𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵
                                                                                               (CS)
                                          𝑥 : 𝐴, 𝑥 : 𝐵 ⊢ 𝑥 : 𝐴 ⇒ 𝐵
                                                                     (∧L)
                                          𝑥:𝐴∧𝐵 ⊢𝑥:𝐴⇒𝐵
                                                                      (→ R)
                                       ⊢ 𝑥 : (𝐴 ∧ 𝐵) → (𝐴 ⇒ 𝐵)

Figure 2: A derivation of CS in SeqS23 .


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 SeqS23 in systems with the rule (CS), then
                                                                                        𝐴′
either (i) Γ ⊢ Δ is derivable in SeqS23 or (ii) 𝑥 = 𝑦 or (iii) there exists 𝑥 −→ 𝑦 ∈ Γ such that
      𝐴′             𝐴
𝑥 −→ 𝑦 ⊢ 𝑥 −→ 𝑦 is derivable in SeqS23 .
                                                                                         𝐴
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,
                          𝐴∨𝐵      ¬𝐴→𝐵                     ¬𝐴→𝐵      ¬𝐴→𝐵
so are the sequents Γ, 𝑥 −→ 𝑦, 𝑥 −→ 𝑧 ⊢ Δ and Γ, 𝑥 −→ 𝑦, 𝑥 −→ 𝑧 ⊢ Δ.
                              𝐴′           𝐴
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:
1
    As 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:
                                                                                𝐴
         (1) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐴            (4) Γ, 𝑥 : 𝐴 ⇒ 𝐵 ⊢ Δ, 𝑥 −→ 𝑥
         (2) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵             (5) Γ, 𝑥 : 𝐴 ⇒ 𝐵, 𝑥 : 𝐵 ⊢ Δ
                                       (CS)                                          (⇒ 𝐿)
            (3) Γ ⊢ Δ, 𝑥 : 𝐴 ⇒ 𝐵                    (6) Γ, 𝑥 : 𝐴 ⇒ 𝐵 ⊢ Δ
                                                                                (𝑐𝑢𝑡)
                                          Γ⊢Δ


   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 𝑥 −→ 𝑦 ⊢ 𝑥 −→ 𝑦 is derivable, we have
           𝐴                                         𝐴′
that Γ′ , 𝑥 −→ 𝑦 ⊢ Δ is derivable, where Γ = Γ′ , 𝑥 −→ 𝑦. By applying the inductive hypothesis
                                                                                              𝐴
on the complexity of the cut formula, we conclude by cutting it with (♠) Γ ⊢ Δ, 𝑥 −→ 𝑦 and
we are done.
                                                                                                      ■

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:

           (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 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].


4. The Theorem Prover CondLean 4.0
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 efficient first-order theorem prover, called leanTAP, 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 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 left-
hand 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)):-
  member([X,A => B],ComplexDelta),
  ∖+member([X,A => B],CS),!,                                                                 (𝑖𝑖𝑖)
  put([X,A],LitDelta,ComplexDelta,LitDelta1,ComplDelta1),
  put([X,B],LitDelta,ComplexDelta,LitDelta2,ComplDelta2),
  prove(Gamma, [LitDelta1,TransDelta,ComplexDelta1],
      Labels, RCond, LCond, [ [X,A => B] | CS], SubTree1),
  prove(Gamma, [LitDelta2,TransDelta,ComplexDelta2],
      Labels, RCond, LCond, [ [X,A => B] | CS], 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 𝑖𝑖𝑖).
   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.
5. 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.


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


References
 [1] D. Lewis, Counterfactuals, Basil Blackwell Ltd (1973).
 [2] D. Nute, Topics in Conditional Logic, Reidel, Dordrecht, 1980.
 [3] R. Stalnaker, A theory of conditionals, in: N. Rescher (Ed.), Studies in Logical Theory,
     Blackwell, 1968, pp. 98–112.
 [4] B. F. Chellas, Basic conditional logics, Journal of Philosophical Logic 4 (1975) 133–153.
 [5] J. P. Burgess, Quick completeness proofs for some logics of conditionals, Notre Dame
     Journal of Formal Logic 22 (1981) 76–84.
 [6] S. Kraus, D. Lehmann, M. Magidor, Nonmonotonic reasoning, preferential models and
     cumulative logics, Artificial Intelligence 44 (1990) 167–207.
 [7] J. P. Delgrande, A first-order conditional logic for prototypical properties, Artificial
     Intelligence 33 (1987) 105–130.
 [8] N. Friedman, J. Y. Halpern, Plausibility measures and default reasoning, Journal of the
     ACM 48 (2001) 648–685.
 [9] L. Giordano, V. Gliozzi, N. Olivetti, G. L. Pozzato, Analytic tableaux for KLM preferential
     and cumulative logics, in: G. Sutcliffe, A. Voronkov (Eds.), Logic for Programming, Artificial
     Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay,
     Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer
     Science, Springer, 2005, pp. 666–681. URL: https://doi.org/10.1007/11591191_46. doi:10.
     1007/11591191\_46.
[10] G. Grahne, Updates and counterfactuals, Journal of Logic and Computation 8 (1998)
     87–117.
[11] L. Giordano, V. Gliozzi, N. Olivetti, Weak agm postulates and strong ramsey test: a logical
     formalization, Artificial Intelligence 168 (2005) 1–37.
[12] L. Giordano, V. Gliozzi, N. Olivetti, Iterated belief revision and conditional logic, Studia
     Logica 70 (2002) 23–47.
[13] D. M. Gabbay, L. Giordano, A. Martelli, N. Olivetti, M. L. Sapino, Conditional reasoning in
     logic programming, Journal of Logic Programming 44 (2000) 37–74.
[14] C. B. Schwind, Causality in action theories, Electronic Transactions on Artificial Intelli-
     gence (ETAI) 3 (1999) 27–50.
[15] L. Giordano, C. Schwind, Conditional logic of actions and causation, Artificial Intelligence
     157 (2004) 239–279.
[16] V. Genovese, L. Giordano, V. Gliozzi, G. L. Pozzato, Logics in access control: a conditional
     approach, Journal of Logic and Computation 24 (2014) 705–762. URL: https://doi.org/10.
     1093/logcom/exs040. doi:10.1093/logcom/exs040.
[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 Re-
     lated 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, Efficient 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: Con-
     ditional 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.

</pre>