Theorem proving for Lewis Logics of Counterfactual Reasoning?

Abstract

We present tuCLEVER, a theorem prover for the strongest conditional logics of counterfactual reasoning introduced by Lewis in the seventies. tuCLEVER implements some hypersequent calculi recently introduced for the system VTU and its main extensions. tuCLEVER is inspired by the methodology of leanTAP and it is implemented in Prolog. Preliminary experimental results show that the performances of tuCLEVER are promising.

Introduction

A

B ! C holds if and only if A ! (B € C) holds where the operator is any update operator satisfying Katsuno and Mendelzon's postulates [ 15 ], that are considered the \core" properties for any concrete, plausible belief-update operator. The relation means that C is entailed by \A updated by B" if and only if the conditional B € C is entailed by A. In this sense it can be said that the conditional B € C expresses an hypothetical update of a ? Copyright c 2020 for this paper by its authors. Use permitted under Creative

Commons License Attribution 4.0 International (CC BY 4.0). piece of information A. They have even been also adopted to reason about access control policies [ 9 ].

One of the most important contribution to conditional logic is due to Lewis. In his seminal work [ 18 ], he proposed a formalization of conditional logics to capture hypothetical conditionals. His aim was to represent conditional sentences that cannot be captured by material implication and, in particular, counterfactuals, e.g. conditionals of the form \if A were the case, then B would be the case", where A is false. In [ 18 ] Lewis introduced a family of conditional logics semantically characterized by sphere models, in which each world x is equipped with a set of nested sets of worlds SP(x). Each set in SP(x) is called a sphere: the intuition is that according to x, worlds in inner spheres are more plausible than worlds belonging only to outer spheres.

Lewis takes as primitive the comparative plausibility operator 4, with a formula A 4 B meaning \A is at least as plausible as B". The conditional A € B is \A is impossible or A ^ :B is less plausible than A ^ B" (where the latter case can be simpli ed to \A ^ :B is less plausible than A"). Vice versa, 4 can be de ned in terms of €.

Here we consider the logics of Lewis' family satisfying two natural properties for hypothetical reasoning and belief change modelling: { Uniformity : all worlds have the same set of accessible worlds, where the worlds accessible from a world x are those belonging to any sphere 2 SP(x); { Total re exivity : every world x belongs to some sphere 2 SP(x). The basic logic is VTU. We also consider some of its extensions, including the above mentioned VCU. It is worth mentioning that equivalent logics are those of Comparative Concept Similarity studied in the context of ontologies [ 25 ]. These logics contain a connective , which allows to express, e.g,

PicassoPainting v BraquePainting

GiottoPainting

asserting that \Picasso's paintings are more similar to Braque's paintings than to Giotto's ones". The semantics is provided in terms of Distance Space Models, de ned as a set of worlds equipped with a distance function. It turns out that the basic logic of Comparative Concept Similarity coincides with Lewis' logic VWU, an extension of the basic system VTU with a property known as weak centering, and the one de ned by \minspace" Distance Models coincides with VCU, so that Distance Space Models provide an alternative simple and natural semantics for conditional logics with uniformity [ 25, 1 ]. All these logics contain modal logic S5 as a fragment: A can be de ned as ? 4 :A (or :A € ?).

In previous works [ 24, 10 ] we proposed some internal sequent calculi for Lewis' logics without Uniformity. Internal calculi are proof methods where each con guration of a derivation corresponds to a formula of the corresponding logic, in contrast to external calculi which make use of extra-logical elements (such as labels, terms and relations on them). We implemented these calculi with the theorem prover VINTE [ 12 ]. However, the mere sequent structure is not powerful enough to capture conditional logic with Uniformity5. In [ 11 ] we proposed the rst proof systems for VTU and its extensions in the form of hypersequent calculi. Hypersequents are nite sets of sequents; and in these calculi sequents are \extended" by a structural connective h:i, representing disjunctions of -formulae.

In this work we present a Prolog implementation of the hypersequent calculi for VTU and its extensions [ 11 ]. The program, called tuCLEVER (Total re exivity and Uniformity Conditional LEwis logics theorem proVER) is, to the best of our knowledge, the only existing prover for conditional logics with Uniformity6. The conception of tuCLEVER is inspired by the methodology of leanTAP [ 3 ]. The idea is that each axiom or rule of the sequent calculi is implemented by a single Prolog clause. No ad-hoc data structure is used. The resulting code is therefore simple and compact: the implementation of tuCLEVER for the basic system VTU consists of only 3 predicates, 21 clauses and 118 lines of code.

The prover provides a decision procedure for the respective logics: it implements the invertible version of the calculi in [ 11 ], where the principal formula or structure is kept in the premises of each rule (similarly to the so-called kleened calculi). In this way, termination is obtained by simply avoiding redundant applications of the rules.

Even if a set of benchmark formulae does not exist, the experimental results obtained so far show that the performances of tuCLEVER are promising. Being the unique theorem prover for conditional logics with Uniformity, tuCLEVER is not directly comparable with any other prover for conditional logics. Nonetheless, we show that on sets of formulae provable in other (weaker) conditional logics and on randomly generated formulas, the performances of tuCLEVER are surprisingly better than the ones of other provers for conditional logics, notably VINTE [ 11 ] which covers weaker logics of the Lewis family. Whether this fact depends on the strength of the logic implemented by tuCLEVER, on the features of the calculi, or on the implementation is an open question.

The program tuCLEVER, as well as all the Prolog source les, are available for free usage and download at http://193.51.60.97:8000/tuclever/.

The article is organized as follows. Section 2 introduces the axioms and the models of the logics under scope. In Section 3 we recall the hypersequent calculi from [ 11 ]. Section 4 presents the design of tuCLEVER, and Section 5 treats its performances. 2

Lewis' Conditional Logics

We consider the conditional logics of [ 18 ]. The set of conditional formulae is given by

A ::= p j ? j > j :A j A ! A j A ^ A j A _ A j A 4 A 5 Conditional logics without Uniformity are PSPACE complete, whereas conditional logics with Uniformity (but without Absoluteness) are EXPTIME complete [ 8 ]. 6 The only possible exception is the theorem prover CSLLean [ 2 ] which implements a calculus for the logic of Comparative Concept Similarity over minspaces, which is equivalent to logic VCU. where p 2 V is a propositional variable. Intuitively, a formula A 4 B is interpreted as \A is at least as plausible as B". Lewis' counterfactual implication € is de ned by A € B (? 4 A) _ :((A ^ :B) 4 A), whereas the outer modality is de ned by A (? 4 :A). The logics we consider are de ned as follows: De nition 1. A model is a triple hW; SP; J: Ki, consisting of a non-empty set W of elements, called worlds, a mapping SP : W ! 22W , and a propositional valuation J: K : V ! 2W . Elements of SP(x) are called spheres. We assume the following conditions: { For every { For every ; { For all w 2 W { For all w 2 W { For all w; v 2 W 2 SP(w) we have 6= ; 2 SP(w) we have or we have SP(w) 6= ; we have w 2 S SP(w) we have S SP(w) = S SP(v) (non-emptiness) (sphere nesting)

(normality) (total re exivity) (uniformity) The valuation J: K is extended to all formulae as follows:

J?K = ; J>K = W J:AK = W JAK JA ^ BK = JAK \ JBK JA _ BK = JAK [ JBK JA ! BK = (W JAK) [ JBK

JA 4 BK = fw 2 W j 8 2 SP(w): if JBK \ 6= ;; then JAK \ 6= ;g Validity and satis ability of formulae in a class of models are de ned as usual. The logic VTU is the set of formulae valid in all models.

We can add to the syntax the conditional operator A € B, since it will be used in formulas handled by the prover. A € B can be de ned in terms of Lewis' plausibility 4 as recalled in the Introduction, and its truth condition is as follows: JA € BK = fw 2 W j either S SP(w) \ JAK = ; or 9 \ JAK 6= ; and \ JAK JBKg.

2 SP(w) such that Extensions of VTU are de ned by adding conditions on the class of models: { For all 2 SP(w) we have w 2 { For all w 2 W we have fwg 2 SP(w) { For all w; v 2 W we have SP(w) = SP(v) (weak centering)

(centering) (absoluteness) Extensions of VTU are denoted by concatenating letters for these properties: W for weak centering, C for centering, and A for absoluteness. We consider7: VTU VWU: VTU + weak centering VCU: VTU + centering

VTA: VTU + absoluteness VWA: VTA + weak centering VCA: VTA + centering

7 Observe that VTA + weak centering collapses to S5, and that VTA + centering collapses to classical logic.

AVTU := f(CPR); (CPA); (TR); (CO); (N); (T); (U1); (U2)g AVWU := AVTU [ f(W)g

AVCU := AVTU [ f(W); (C)g

AVTA := AVTU [ f(A1); (A2)g AVWA := AVTU [ f(W); (A1); (A2)g

AVCA := AVTU [ f(W); (C); (A1); (A2)g

These logics can be characterized by axioms in a Hilbert-style system [18, Chp. 6]. The modal axioms in the language with only the comparative plausibility operator are given in Table 1 (_ and ^ bind stronger than 4). Propositional axioms and rules are standard. 3

Hypersequent Calculi for Lewis' Logics

We recall hypersequent calculi for VTU and extensions from [ 11 ]. These calculi are based on hypersequents, namely non-empty, nite multisets of extended sequents. The extended sequents contain in the succedent a structural connective h:i interpreting possible formulae.

Formally, we de ne: { a conditional block, which is a tuple [ C C] containing a nite multiset of formulae and a single formula C; { a transfer block, which is a nite multiset of formulae, written h i; { an extended sequent, which is a tuple ) consisting of a nite multiset of formulae and a nite multiset containing formulae, conditional blocks, and transfer blocks; { an extended hypersequent, which is a nite multiset containing extended sequents, written 1 ) 1 j : : : j n ) n.

The rules of the calculi introduced in [ 11 ] are shown in Fig. 1. Given A :(? 4 A), the formula interpretation of an extended sequent and of an extended hypersequent are given by: e( ) ; [ 1 C C1] ; : : : ; [ n C Cn] ; h 1i ; : : : ; h mi) := V ! W _ Win=1 WB2 i(B 4 Ci) _ Wjm=1 (W j) e( 1 ) 1 j : : : j n ) n) := e( 1 ) 1) _ _ e( n ) n): Theorem 2 (Soundness and Completeness). For A formula, A 2 L if and only if SHiL ` ) A.

The calculi of Fig. 1 can be used to de ne a decision procedure for the corresponding logics.

; h?i intirf G j )

G j ) G j ) ; [ C A] ;

G j ) ; [ C A] G j ; A 4 B )

G j ; A 4 B ) j

G j

G j

Wi ) j ; A 4 B ) G j ; ? ) ?L

G j ) ; > >R

G j ; p ) SHiVTA = SHiVTU [ fabsiL; absiRg SHiVWA = SHiVWU [ fabsiL; absiRg

SHiVCA = SHiVCU [ fabsiL; absiRg In this section we present a Prolog implementation of the hypersequent calculi recalled in Section 3. The program, called tuCLEVER, is inspired by the \lean" methodology of leanTAP, even if it does not follow its style in a rigorous manner. _iL The program comprises a set of clauses, each of them implementing a sequent rule or axiom of the calculi. tuCLEVER implements a cumulative, or kleened, version of the calculi SHiL, in which each rule keeps its principal formula in the premises. In this way, termination is ensured in an immediate way by checking redundancy of the rules applications. The proof search is provided for free by the mere depth- rst search mechanism of Prolog, without any additional ad hoc mechanism.

tuCLEVER represents an hypersequent as a Prolog list of extended sequents. In turn, an extended sequent is represented as a pair of Prolog lists [Gamma,Delta], where Gamma and Delta represent the left-hand and the right-hand side of the extended sequent, respectively. An extended sequent contains conditional blocks and transfer blocks. A conditional block [ C C] is a pair [Sigma,C], i.e. a Prolog list with two elements, where Sigma is a list of formulas. A transfer block h i is implemented by a term transfer Theta, where again Theta is a Prolog list. Symbols > and ? are represented by constants true and false, respectively, whereas connectives :, ^, _, !, 4, and € are represented by -, and, or, ->, <, and =>. Propositional variables are represented by Prolog atoms. As an example, the sequent A; :B _ C ) A ^ C; D; A ! B; h?i; [A 4 C; B C A _ C] is represented by the list: [[a; b or c]; [a and c; d; a > b; transfer[false]; [[a < c; b]; a or c]]]: The hypersequent calculi are implemented for each logic by the predicate prove(Hypersequent,ProofTree).

This predicate succeeds if and only if the hypersequent represented by the list Hypersequent is derivable. When it succeeds, the output term ProofTree matches with a representation of the derivation found by the prover. For instance, in order to prove the formula (A 4 A _ B) _ (B 4 A _ B) in VTU, one queries tuCLEVER with the goal: prove([[],[(a < a or b) or (b < a or b)]],ProofTree). Each clause of prove implements an axiom or rule of the calculi in Figure 1. To search a derivation, tuCLEVER proceeds as follows. First of all, if the hypersequent is an instance of either ?L or >R or init, the goal will succeed immediately by using one of the following clauses for the axioms: prove(Hypersequent,tree(...)) :

member([Gamma,Delta],Hypersequent),member(false,Gamma),!. prove(Hypersequent,tree(...)) :

member([Gamma,Delta],Hypersequent),member(true,Delta),!. prove(Hypersequent,tree(...)) :- member([Gamma,Delta],Hypersequent), member(X,Gamma),member(X,Delta),atom(X),!.

If the hypersequent is not an instance of the ending rules, then the rst applicable rule will be chosen, e.g. if a sequent ) contains a formula A < B in the right-hand side , then the clause implementing the 4iR rule will be chosen, and tuCLEVER will be recursively invoked on the unique premise of such a rule introducing a conditional block [A C B]. tuCLEVER proceeds in a similar way for the other rules. The ordering of the clauses is such that the application of the branching rules is postponed as much as possible. As an example, the clause implementing 4iR is as follows: 1. prove(Hypersequent,tree(condR,Hypersequent,[Gamma,Delta],no, SubTree1,no)) :2. select([Gamma,Delta],Hypersequent,Remainder), 3. member(A < B, Delta), 4. \+findBlock(Delta,[[A],B]),!, 5. prove([[Gamma,[[[A],B]|Delta]]|Remainder],SubTree1). In line 4, the auxiliary predicate findBlock is invoked in order to implement the decision procedure described at the beginning of this section: if a conditional block [A C B], represented by the Prolog pair [[A],B], already belongs to , then the negation as failure returns a failure, and the rule is no longer applied. Since the rule is invertible, Prolog cut ! is used in line 4 to eventually block backtracking.

As an another example, the following clause implements the rule jumpiU : 1. prove(Hypersequent,tree(jumpU,Hypersequent,[Gamma,Delta], [Gamma2,Delta2],SubTree1,no)) :2. select([Gamma,Delta],Hypersequent,Remainder), 3. member(transfer Theta, Delta), 4. select([Gamma2,Delta2],Remainder,Remainder2), 5. \+subset(Theta,Delta2), 6. append(Delta2,Theta,NewDelta2), 7. !, 8. prove([[Gamma,Delta],[Gamma2,NewDelta2]|Remainder2],SubTree1). In line 3, the predicate member checks whether there is a block h i, represented by the Prolog term transfer Theta, in this case the main predicate is recursively invoked on the only premise of the rule, by adding formulas in in the right hand side of the sequent represented by Gamma2 and Delta2.

Implementations of the calculi for extensions of VTU proceed in a similar way. To show some examples, here are the clauses implementing the rules Wi and Ti, belonging to the implementations of the systems involving axioms W and C. 1. prove(Hypersequent,tree(w,Hypersequent,[Gamma,Delta],no, SubTree1,no)) :2. select([Gamma,Delta],Hypersequent,Remainder), 3. member([Sigma,_],Delta), 4. \+subset(Sigma,Delta), 6. append(Delta,Sigma,NewDelta),!, 7. prove([[Gamma,NewDelta]|Remainder],SubTree1).

In line 4 the predicate n+subset(Sigma,Delta) checks whether , represented by the Prolog list Sigma, belongs to , represented by the Prolog list Delta, in order to avoid multiple applications of the rule over the same set .

The Prolog source code implementing the rule Ti is as follows: 1. prove(Hypersequent,tree(t,Hypersequent,[Gamma,Delta],no, SubTree1,SubTree2)) :2. 3. 4. 5. 6. 7. 8. 9. select([Gamma,Delta],Hypersequent,Remainder), member(A < B,Gamma), select(transfer Theta,Delta,Delta2), \+member(B,Theta), \+findSequent(Hypersequent,[[A],Theta]), !, prove([[Gamma,Delta],[[A],Theta]|Remainder],SubTree1), prove([[Gamma,[transfer [B|Theta]|Delta2]]|Remainder], SubTree2).

In line 8 an extended sequent A ) is added as a new component of the hypersequent, whereas in line 9 the formula B is added to h i in the right-hand side of the sequent under consideration. Lines 5 and 6 are used in order to implement the decision procedure, by avoiding useless applications of the rule in case either B already belongs to or an extended sequent A ) h i already exists in the hypersequent.

Let us conclude by showing the Prolog clauses implementing the rules absiL and absiR characterizing the systems allowing the axiom A. 1. prove(Hypersequent,tree(absL,Hypersequent,[Gamma,Delta], [Gamma2,Delta2],SubTree1,no)) :2. select([Gamma,Delta],Hypersequent,Remainder), 3. member(A < B,Gamma), 4. select([Gamma2,Delta2],Remanider,Remainder2), 5. \+member(A < B,Gamma2), 6. !, 7. prove([[Gamma,Delta],[[A < B|Gamma2],Delta2]!Remainder2], SubTree1). 1. prove(Hypersequent,tree(absR,Hypersequent,[Gamma,Delta], [Gamma,Delta],SubTree1,no)) :2. select([Gamma,Delta],Hypersequent,Remainder), 3. member(A < B,Delta), 4. select([Gamma2,Delta2],Remainder,Remainder2), 5. \+member(A < B,Delta2), 6. !, 7. prove([[Gamma,Delta],[Gamma2,[A < B|Delta2]]|Remainder2], SubTree1).

The system tuCLEVER has also a graphical user interface implemented in the form of a responsive Web Application. As already mentioned in the Introduction, the program tuCLEVER, as well as all the Prolog source les, are available for free usage and download at http://193.51.60.97:8000/tuclever/. 5

Performance of tuCLEVER

The performance of tuCLEVER are promising. We have tested it by running SWI Prolog 7.6.4 on an Acer Aspire E5-575G, 2.7 GHz Intel Core i7 7500U, 16GB

RAM, Ubuntu 19.04 amd64 machine. In absence of theorem provers speci cally tailored for Lewis' logics, we have compared the performances of tuCLEVER with those of VINTE [ 12 ] on formulas provable in both systems. We have performed two kinds of experiments. On the one hand, we have tested the two provers over a set of valid formulas, on the other hand we have tested tuCLEVER with randomly generated formulas, therefore including not provable ones. First of all, we have tested both tuCLEVER and VINTE over 76 valid formulas in the basic Lewis' system V without Uniformity [ 18 ], obtained by translating valid formulas of the basic modal logic K [ 14 ] provided by Heuerding in conditional formulas: A is replaced by > € A8, whereas A is replaced by :(> € :A). We have observed the results in Figure 6 concerning the number of timeouts, witnessing a signi cant increase of performances with respect to those of VINTE. 8 It is worth noticing that this translation introduces an exponential blowup.

Theorem prover 1 s 60 s 180 s

VINTE 49 34 31 tuCLEVER 8 3 3

This result could be explained by the fact that, even if tuCLEVER manipulates \heavier" hypersequents, all rules implemented by tuCLEVER are invertible, avoiding backtracking points that are present in VINTE.

We have then compared the performance of both the provers tuCLEVER and VINTE with valid formulas obtained as instances of three di erent schemas, by xing a time limit of 60 seconds, and by letting a parameter n vary, starting from n = 1. The rst schema is as follows: (A1 4 A2) _ (A2 4 A3) _ _ (An 4 A1); We have observed that tuCLEVER is able to answer also with n = 25, whereas VINTE is able to answer only until n = 9. Similarly, we have compared the performance of the provers on: (A1 4 A2) ^ (A2 4 A3) ^

^ (An 1 4 An) ! (A1 4 An) obtaining that tuCLEVER is able to answer also with n = 15, whereas VINTE is able to answer only until n = 5. The prover VINTE has, however, better performances than those of tuCLEVER over formulas following the following schema: (A1 4 (A1 _ A2 _ _ An)) _ (A2 4 (A1 _ A2 _ : : : _ (An 4 (A1 _ A2 _ _ An)) _ An)) _ : : : where tuCLEVER is able to answer with n = 4, whereas VINTE is able to answer also for n = 15. 5.2

Tests over randomly generated formulas We have tested tuCLEVER over randomly generated formulas, xing two di erent time limits, namely 1 second and 10 seconds, and varying the depth of a formula (i.e. the maximum level of nesting of connectives) as well as the number of di erent propositional variables. We have considered the system VTU as well as all the extensions, obtaining the percentages of timeouts in Figures 7 and 8. In all cases, the quite low percentages of timeouts suggest that the performance of tuCLEVER are encouraging. 6

Conclusions and Future Issues

We have introduced tuCLEVER, a theorem prover implementing hypersequent calculi for Lewis' conditional logics with Total Re exivity and Uniformity introduced in [ 11 ]. As far as we know, this is the rst theorem prover for these stronger logics of the Lewis' family. Depth / var 1 s 10 s 5/3 0% 0% 6/3 2% 0% 7/3 4% 2% 8/3 7% 5% 5/5 0% 0% 6/5 2% 1% 7/5 6% 4% 8/5 10% 7%

We have compared the performance of tuCLEVER with those of VINTE, a theorem prover for the weaker Lewis' logics, and we have observed that the performance of tuCLEVER are promising. We aim at extending our performance evaluation by considering other signi cant schemas of valid formulas: as an example, we plan to consider valid formulas obtained by the translations of the rules Rn;m of the sequent calculus for V according to the translation from rules to axioms described in [ 17 ]. Furthermore, we aim at comparing the performance of tuCLEVER also with those of other provers for conditional logic, like CondLean [ 21 ], GoalDUCK [ 20 ], and NESCOND [ 22, 23 ]. As already mentioned, the theorem prover CSLLean [ 2 ] implements a labelled calculus for the logic of Comparative Concept Similarity over minspaces, which is equivalent to logic VCU: we aim at comparing tuCLEVER with CSLLean, by repeating tests both over randomly generated formulas and over valid VCU formulas.

Finally, we are currently working on extending tuCLEVER in order to handle countermodel generation for unprovable formulas: intuitively, given a failed proof, tuCLEVER checks another Prolog predicate essentially implementing the same clauses of prove, with the objective of nding an open, saturated branch, following the line of the theorem provers for Lewis' logics of counterfactual reasoning [ 6, 7 ]. Clauses introducing a branch in the computation, i.e. those implementing rules with two premises, are split in two clauses, each one considering a single branch. The last clause of this additional Prolog predicate will check whether the hypersequent is not an instance of the initial sequents: in this way, this predicate will succeed if and only if (i) no rule of the calculi is further applicable (ii) the hypersequent does not contain a valid extended sequent, therefore a model falsifying it can be extracted from the sequent itself.

Acknowledgements

This work is partially supported by the Projects TICAMORE ANR-16-CE91-000201, WWTF project MA16-28, and INDAM-GNCS \METALLIC #2" INDAMGNCS Project 2020.

References

1. Alenda , R. , Olivetti , N.: Preferential semantics for the logic of comparative similarity over triangular and metric models . In: del Cerro , L.F. , Herzig , A. , Mengin , J . (eds.) JELIA 2012 , LNAI , vol. 7519 , pp. 1 { 13 . Springer-Verlag Berlin Heidelberg ( 2012 )

2. Alenda , R. , Olivetti , N. , Pozzato , G.L. : Csl-lean: A theorem-prover for the logic of comparative concept similarity . Electr. Notes Theor. Comput. Sci. 262 , 3 { 16 ( 2010 ), https://doi.org/10.1016/j.entcs. 2010 . 04 .002

3. Beckert , B. , Posegga , J.: leantap: Lean tableau-based deduction . Journal of Automated Reasoning 15 ( 3 ), 339 { 358 ( 1995 )

4. Burgess , J.P. : Quick completeness proofs for some logics of conditionals . Notre Dame Journal of Formal Logic 22 , 76 { 84 ( 1981 )

5. Chellas , B.F. : Basic conditional logics . Journal of Philosophical Logic 4 , 133 { 153 ( 1975 )

6. Dalmonte , T. , Negri , S. , Olivetti , N. , Pozzato , G.L. : PRONOM: proof-search and countermodel generation for non-normal modal logics . In: Alviano, M. , Greco , G. , Scarcello , F . (eds.) AI*IA 2019 - Advances in Arti cial Intelligence - XVIIIth International Conference of the Italian Association for Arti cial Intelligence , Rende, Italy, November 19-22 , 2019 , Proceedings. Lecture Notes in Computer Science , vol. 11946 , pp. 165 { 179 . Springer ( 2019 ), https://doi.org/10.1007/978-3- 030 -35166-3 12

7. Dalmonte , T. , Olivetti , N. , Pozzato , G.L. : HYPNO: theorem proving with hypersequent calculi for non-normal modal logics (system description) . In: Peltier, N. , Sofronie-Stokkermans , V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020 , Paris, France, July 1-4 , 2020 , Proceedings, Part II. Lecture Notes in Computer Science , vol. 12167 , pp. 378 { 387 . Springer ( 2020 ), https://doi.org/10.1007/978-3- 030 -51054-1 23

8. Friedman , N. , Halpern , J.Y.: On the complexity of conditional logics . In: Principles of Knowledge Representation and Reasoning . pp. 202 { 213 . Elsevier ( 1994 )

9. Genovese , V. , Giordano , L. , Gliozzi , V. , Pozzato , G.L. : Logics in access control: a conditional approach . Journal of Logic and Computation 24 ( 4 ), 705 { 762 ( 2014 )

10. Girlando , M. , Lellmann , B. , Olivetti , N. , Pozzato , G.L. : Standard sequent calculi for Lewis' logics of counterfactuals . In: Logics in Arti cial Intelligence . JELIA 2016 ., vol. 10021 , pp. 272 { 287 . Springer ( 2016 )

11. Girlando , M. , Lellmann , B. , Olivetti , N. , Pozzato , G.L. : Hypersequent calculi for lewis' conditional logics with uniformity and re exivity . In: Schmidt, R.A. , Nalon , C. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017 , Bras lia , Brazil, September 25-28 , 2017 , Proceedings. Lecture Notes in Computer Science , vol. 10501 , pp. 131 { 148 . Springer ( 2017 ), https://doi.org/10.1007/978-3- 319 -66902-1 8

12. Girlando , M. , Lellmann , B. , Olivetti , N. , Pozzato , G.L. , Vitalis , Q. : VINTE: an implementation of internal calculi for lewis' logics of counterfactual reasoning . In: Schmidt, R.A. , Nalon , C. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 26th International Conference, TABLEAUX 2017 , Bras lia , Brazil, September 25-28 , 2017 , Proceedings. Lecture Notes in Computer Science , vol. 10501 , pp. 149 { 159 . Springer ( 2017 ), https://doi.org/10.1007/978-3- 319 -66902-1 9

13. Grahne , G.: Updates and counterfactuals . Journal of Logic and Computation 8 ( 1 ), 87 { 117 ( 1998 )

14. Hughes , G. , Cresswell , J.: An Introduction to Modal Logic . Methuen ( 1968 )

15. Katsuno , H. , Mendelzon , A.O. : On the di erence between updating a knowledge base and revising it . In: Allen, J.F. , Fikes , R. , Sandewall , E. (eds.) Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning (KR'91) . Cambridge, MA, USA, April 22 - 25 , 1991 . pp. 387 { 394 . Morgan Kaufmann ( 1991 )

16. Kraus , S. , Lehmann , D. , Magidor , M. : Nonmonotonic reasoning, preferential models and cumulative logics . Arti cial Intelligence 44 ( 1-2 ), 167 { 207 ( 1990 )

17. Lellmann , B. , Pattinson , D. : Correspondence between modal hilbert axioms and sequent rules with an application to S5 . In: Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013 , Nancy, France, September 16-19 , 2013 . Proceedings. Lecture Notes in Computer Science , vol. 8123 , pp. 219 { 233 . Springer ( 2013 )

18. Lewis , D. : Counterfactuals. Blackwell ( 1973 )

19. Nute , D. : Topics in Conditional Logic. Reidel, Dordrecht ( 1980 )

20. Olivetti , N. , Pozzato , G.L. : Theorem Proving for Conditional Logics: CondLean and GoalDuck . J. of Applied Non-Classical Logics 18 ( 4 ), 427 { 473 ( 2008 )

21. Olivetti , N. , Pozzato , G.L. : Condlean 3.0: Improving condlean for stronger conditional logics . In: Beckert, B . (ed.) Automated Reasoning with Analytic Tableaux and Related Methods , International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17 , 2005 , Proceedings. Lecture Notes in Computer Science , vol. 3702 , pp. 328 { 332 . Springer ( 2005 ), https://doi.org/10.1007/11554554 27

22. Olivetti , N. , Pozzato , G.L. : NESCOND: an implementation of nested sequent calculi for conditional logics . In: Demri, S. , Kapur , D. , Weidenbach , C. (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014 , Held as Part of the Vienna Summer of Logic , VSL 2014 , Vienna, Austria, July 19-22 , 2014 . Proceedings. Lecture Notes in Computer Science , vol. 8562 , pp. 511 { 518 . Springer ( 2014 ), https://doi.org/10.1007/978-3- 319 -08587-6 39

23. Olivetti , N. , Pozzato , G.L. : Nested sequent calculi and theorem proving for normal conditional logics: The theorem prover NESCOND . Intelligenza Arti ciale 9(2) , 109 { 125 ( 2015 )

24. Olivetti , N. , Pozzato , G.L.: A standard internal calculus for lewis' counterfactual logics . In: de Nivelle, H. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015 , Wroclaw, Poland, September 21-24 , 2015 . Proceedings, Lecture Notes in Computer Science , vol. 9323 , pp. 270 { 286 . Springer ( 2015 ), https://doi.org/10.1007/978-3- 319 -24312- 2 19

25. Sheremet , M. , Tishkovsky , D. , Wolter , F. , Zakharyaschev , M.: A logic for concepts and similarity . J. Log. Comput . 17 ( 3 ), 415 { 452 ( 2007 )

26. Stalnaker , R.: A theory of conditionals . In: Rescher, N. (ed.) Studies in Logical Theory , pp. 98 { 112 . Blackwell ( 1968 )