=Paper=
{{Paper
|id=None
|storemode=property
|title=Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-l04.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/OlivettiP13
}}
==Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics==
https://ceur-ws.org/Vol-1068/paper-l04.pdf
Nested Sequent Calculi and Theorem Proving for
Normal Conditional Logics
Nicola Olivetti1 and Gian Luca Pozzato2
1
Aix-Marseille Université, CNRS, LSIS UMR 7296 - France - nicola.olivetti@univ-amu.fr
2
Dipartimento di Informatica - Università di Torino - Italy gianluca.pozzato@unito.it
Abstract. In this paper we focus on proof methods and theorem proving for nor-
mal conditional logics, by describing nested sequent calculi as well as a theorem
prover for them. Nested sequent calculi are a useful generalization of ordinary se-
quent calculi, where sequents are allowed to occur within sequents. Nested sequent
calculi have been profitably employed in the area of (multi)-modal logic to obtain
analytic and modular proof systems for these logics. In this work, we describe
nested sequent calculi recently introduced for the basic conditional logic CK and
some of its significant extensions. We also provide a calculus for Kraus Lehman
Magidor cumulative logic C. The calculi are internal (a sequent can be directly
translated into a formula), cut-free and analytic. Moreover, they can be used to
design (sometimes optimal) decision procedures for the respective logics, and to
obtain complexity upper bounds. Our calculi are an argument in favour of nested
sequent calculi for modal logics and alike, showing their versatility and power.
We also describe NESCOND, a Prolog implementation of nested sequent calculi
mentioned above. NESCOND (NESted sequent calculi for propositional CONDi-
tional logics) is inspired by the methodolody of leanTAP. The paper also shows
some experimental results, witnessing that the performances of NESCOND are
promising. NESCOND is available at http://www.di.unito.it/∼pozzato/nescond/
1 Introduction
Conditional logics extend classical logic by means of a conditional operator ⇒. They can
be seen as a generalization of (multi)modal logics, where the modality ⇒ is indexed by
a formula of the same language. Conditional logics have a long history: Lewis [15, 16]
introduced them in order to formalize a kind of hypothetical reasoning: the conditional
formula A ⇒ B is used to formalize a sentence like “if A were the case then B” that
cannot be captured by classical logic with material implication. One original motivation
was to formalize counterfactual sentences, i.e. conditionals of the form “if A were the
case then B would be the case”, where A is false.
Over the years, conditional logics firmly established themselves in various fields of
artificial intelligence and knowledge representation. Just to mention a few, they have
been used3 to reason about prototypical properties [10] and to model belief change [12,
11]. Moreover, they can provide an axiomatic foundation of nonmonotonic reasoning
[7, 14]: in detail, a conditional A ⇒ B is read as “in normal circumstances, if A then
B”. Recently, constructive conditional logics have been applied to reason about access
control policies [9, 8]: the statement A says B, intuitively meaning that a user/program
3
We refer to [20, 1] for a complete bibliography about conditional logics.
50 Nicola Olivetti and Gian Luca Pozzato
A asserts B to hold in the system, can be naturally expressed by a conditional A ⇒ B.
Finally, a kind of (multi)-conditional logics [3, 6] have been used to formalize epistemic
change in a multi-agent setting and in some kind of epistemic “games”, each conditional
operator expresses the “conditional beliefs” of an agent.
All conditional logics enjoy a possible world semantics, with the intuition that a
conditional A ⇒ B is true in a world x if B is true in the set of worlds where A is true
and that are most similar to/closest to/“as normal as” x. Since there are different ways of
formalizing “the set of worlds similar/closest/...” to a given world, there are expectedly
rather different semantics for conditional logics, from the most general selection function
semantics to the stronger sphere semantics.
However, from the point of view of proof-theory and automated deduction, con-
ditional logics have not achieved a state of the art comparable with, say, the one of
modal logics, where there are well-established calculi, whose proof-theoretical and
computational properties are well-understood. In this work we first describe nested
sequent calculi, called N S, for propositional conditional logics, recently introduced in
[1, 2]. Nested sequent calculi, introduced by Kashima in [13] for classical modal logics,
are a natural generalization of ordinary sequent calculi where sequents are allowed to
occur within sequents. However, a nested sequent always corresponds to a formula of the
language, so that we can think of the rules as operating “inside a formula”, combining
subformulas rather than just combining outer occurrences of formulas as in ordinary
sequent calculi.
We will consider the basic normal conditional logic CK and its extensions with ID,
MP and CEM, as well as the cumulative logic C introduced in [14] which corresponds
to the flat fragment (i.e., without nested conditionals) of CK+CSO+ID. The calculi are
rather natural, all rules have a fixed number of premises. Completeness is established
by cut-elimination, whose peculiarity is that it must take into account the substitution
of equivalent antecedents of conditionals (a condition corresponding to normality). The
calculi can be used to obtain a decision procedure for the respective logics by imposing
some restrictions preventing redundant applications of rules. In all cases, we get a
PS PACE upper bound, a bound that for CK and its extensions with ID and MP is optimal
(but not for CK+CEM that is known to be CO NP). For flat CK+CSO+ID = cumulative
logic C we also get a PS PACE bound, we are not aware of a better upper bound for this
logic (although we may suspect that it is not optimal).
Furthermore, we describe an implementation of N S calculi in Prolog. The program,
called NESCOND, gives a PS PACE decision procedure for the respective logics, and it is
inspired by the methodology introduced by the system leanTAP [4], even if it does not
fit its style in a rigorous manner. The basic idea is that each axiom or rule of the nested
sequent calculi is implemented by a Prolog clause of the program. The resulting code is
therefore simple and compact: the implementation of NESCOND for CK consists of only
6 predicates, 24 clauses and 34 lines of code. We also provide some experimental results
to show that the performances of NESCOND are promising, especially compared to the
ones of CondLean [17, 18] and G OAL DUCK [19], to the best of our knowledge the only
existing provers for conditional logics. This shows that nested sequent calculi are not
only a proof theoretical tool, but they can be the basis of efficient theorem proving for
conditional logics.
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 51
2 Normal Conditional Logics
We consider a propositional conditional language L over a set ATM of propositional
variables. Formulas of L are built as usual: ⊥, > and the propositional variables in
ATM are atomic formulas; if A and B are formulas, then ¬A and A ⊗ B are compound
formulae, where ⊗ ∈ {∧, ∨, →, ⇒}. We adopt the selection function semantics.
Definition 1 (Selection function semantics). A model is a triple M = hW, f, [ ]i:
– W is a non empty set of worlds;
– f : W × 2W 7−→ 2W is the selection function;
– [ ] is the evaluation function, which assigns to an atom P ∈ ATM the set of worlds
where P is true, and is extended to boolean formulas as follows:
• [>] = W;
• [⊥] = ∅;
• [¬A] = W − [A];
• [A ∧ B] = [A] ∩ [B];
• [A ∨ B] = [A] ∪ [B];
• [A → B] = [B] ∪ (W − [A]);
• [A ⇒ B] = {w ∈ W | f (w, [A]) ⊆ [B]}.
A formula F ∈ L is valid in a model M = hW, f, [ ]i, and we write M |= F , if
[F ] = W. A formula F ∈ L is valid, and we write |= F , if it is valid in every model,
that is to say M |= F for every M.
The semantics above characterizes the basic conditional system, called CK, where no
specific properties of the selection function are assumed. An axiomatization of CK is
given by (` denotes provability in the axiom system):
– any axiomatization of the classical propositional calculus (prop)
– If ` A and ` A → B, then ` B (Modus Ponens)
– If ` A ↔ B then ` (A ⇒ C) ↔ (B ⇒ C) (RCEA)
– If ` (A1 ∧ · · · ∧ An ) → B then ` (C ⇒ A1 ∧ · · · ∧ C ⇒ An ) → (C ⇒ B) (RCK)
Moreover, we consider the following standard extensions of the basic system CK:
System Axiom Model condition
ID A⇒A f (w, [A]) ⊆ [A]
CEM (A ⇒ B) ∨ (A ⇒ ¬B) | f (w, [A]) |≤ 1
MP (A ⇒ B) → (A → B) w ∈ [A] implies w ∈ f (w, [A])
(A ⇒ B)∧(B ⇒ A) → ((A ⇒ C) → f (w, [A]) ⊆ [B] and f (w, [B]) ⊆ [A] implies
CSO (B ⇒ C)) f (w, [A]) = f (w, [B])
3 Nested Sequent Calculi N S for Conditional Logics
In this section we recall nested sequent calculi N S introduced in [1, 2], where S is an
abbreviation for CK{+X}, with X ∈ {CEM, ID, MP, ID+MP, CEM+ID}. We are able to
deal with the basic normal conditional logic CK and its extensions with axioms ID, MP
and CEM. We are also able to deal with some combinations of them, namely the systems
allowing ID with either MP or CEM. The problem of extending N S to the conditional
52 Nicola Olivetti and Gian Luca Pozzato
Γ(P, ¬P ) (AX) Γ(⊤) (AX⊤ ) Γ(¬⊥) (AX⊥ ) Γ(A)
(¬)
P ∈ ATM Γ(¬¬A)
Γ(A) Γ(B) Γ(¬A, ¬B) Γ(A, B) Γ(¬A) Γ(¬B)
(∧+ ) (∧− ) (∨+ ) (∨− )
Γ(A ∧ B) Γ(¬(A ∧ B)) Γ(A ∨ B) Γ(¬(A ∨ B))
Γ(¬A, B) Γ(A) Γ(¬B) Γ(¬(A ⇒ B), [A′ : ∆, ¬B]) A, ¬A′ A′ , ¬A
(→+ ) (→− ) (⇒− )
Γ(A → B) Γ(¬(A → B)) Γ(¬(A ⇒ B), [A′ : ∆])
Γ([A : B]) + Γ(¬(A ⇒ B), A) Γ(¬(A ⇒ B), ¬B) Γ([A : ∆, Σ], [B : Σ]) A, ¬B B, ¬A
(⇒ ) (M P ) (CEM )
Γ(A ⇒ B) Γ(¬(A ⇒ B)) Γ([A : ∆], [B : Σ])
Γ([A : ∆, ¬A]) Γ, ¬(A ⇒ B), [A′ : ∆, ¬B] Γ, ¬(A ⇒ B), [A : A′ ] Γ, ¬(A ⇒ B), [A′ : A]
(ID) (CSO)
Γ([A : ∆]) Γ, ¬(A ⇒ B), [A′ : ∆]
Fig. 1. The nested sequent calculi N S.
logics allowing both MP and CEM is open at present. As usual, the completeness of
the calculi is an easy consequence of the admissibility of cut. We are also able to turn
N S into a terminating calculus, which gives us a decision procedure for the respective
conditional logics.
A nested sequent Γ is defined inductively as follows:
– a formula of L is a nested sequent;
– if A is a formula and Γ is a nested sequent, then [A : Γ ] is a nested sequent;
– a finite multiset of nested sequents is a nested sequent.
A nested sequent can be displayed as
A1 , . . . , Am , [B1 : Γ1 ], . . . , [Bn : Γn ],
where n, m ≥ 0, A1 , . . . , Am , B1 , . . . , Bn are formulas and Γ1 , . . . , Γn are nested
sequents.
A nested sequent can be directly interpreted as a formula, just replace “,” by ∨
and “:” by ⇒. More explicitly, the interpretation of a nested sequent A1 , . . . , Am , [B1 :
Γ1 ], . . . , [Bn : Γn ] is inductively defined by the formula
F(Γ ) = A1 ∨ . . . ∨ Am ∨ (B1 ⇒ F(Γ1 )) ∨ . . . ∨ (Bn ⇒ F(Γn )).
The calculi N S are shown in Figure 1. As usual, we say that a nested sequent Γ is
derivable in N S if it admits a derivation. A derivation is a tree whose nodes are nested
sequents. A branch is a sequence of nodes Γ1 , Γ2 , . . . , Γn , . . . such that each node Γi is
obtained from its immediate successor Γi−1 by applying backward a rule of N S, having
Γi−1 as the conclusion and Γi as one of its premises. A branch is closed if one of its
nodes is an instance of axioms (AX), (AX> ), (AX⊥ ), otherwise it is open. We say that
a tree is closed if all its branches are closed. A nested sequent Γ has a derivation in N S
if there is a closed tree having Γ as the root. As an example, Figure 2 shows a derivation
in the calculus N CK+ID of an instance of the axiom ID.
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 53
(AX)
[P : P, ¬P ]
(ID)
[P : P ]
(⇒+ )
P ⇒P
Fig. 2. A derivation of an instance of the axiom ID in N CK+ID.
We have also provided a nested sequent calculus for the flat fragment, i.e. without nested
conditionals, of CK+CSO+ID, corresponding to KLM logic C. The rules of the calculus,
called N CKLM , are those ones of N CK+ID (restricted to the flat fragment) where the
rule (⇒− ) is replaced by the rule (CSO).
The specificity of nested sequent calculi is to allow inferences that apply within
sequence. In order to introduce the rules of the calculus, we need the notion of context.
Intuitively a context denotes a “hole”, a unique empty position, within a sequent that
can be filled by a sequent. We use the symbol ( ) to denote the empty context. A context
is defined inductively as follows: Γ ( ) = Λ, ( ) is a context; if Σ( ) is a context,
Γ ( ) = Λ, [A : Σ( )] is a context. Finally, we define the result of filling “the hole” of a
context by a sequent. Let Γ ( ) be a context and ∆ be a sequent, then the sequent obtained
by filling the context by ∆, denoted by Γ (∆) is defined as follows: if Γ ( ) = Λ, ( ),
then Γ (∆) = Λ, ∆; if Γ ( ) = Λ, [A : Σ( )] then Γ (∆) = Λ, [A : Σ(∆)]. The notions
of derivation and of derivable sequent are defined as usual.
Nested sequent calculi N S are sound and complete with respect to the semantics for
the respective logics.
Theorem 1. The nested sequent calculi N S are sound and complete for the respective
logics, i.e. a formula F of L is valid in CK+X if and only if it is derivable in N CK+X.
Proof. (Soundness): If Γ is derivable in N S, then Γ is valid. To improve readability, we
slightly abuse the notation identifying a sequent Γ with its interpreting formula F(Γ ),
thus we shall write A ⇒ ∆, Γ ∧ ∆, etc. instead of A ⇒ F(∆), F(Γ ) ∧ F(∆). First, we
prove that nested inference is sound, that is to say: let Γ ( ) be any context. If the formula
A1 ∧ . . . ∧ An → B, with n ≥ 0, is (CK{+X})-valid, then also Γ (A1 ) ∧ . . . ∧ Γ (An ) →
Γ (B) is (CK{+X}) valid. The proof is by induction on the depth of a context Γ ( ),
defined as follows:
– Γ ( ) = ∆, ( ) is a context with depth d(Γ ( )) = 0;
– if Σ( ) is a context, Γ ( ) = ∆, [A : Σ( )] is a context with depth d(Γ ( )) =
1 + d(Σ( )).
Let d(Γ ( )) = 0, then Γ = Λ, ( ). Since A1 ∧ . . . ∧ An → B is valid, by propositional
reasoning, we have that also (Λ ∨ A1 ) ∧ . . . (Λ ∨ An ) → (Λ ∨ B) is valid, that is
Γ (A1 ) ∧ . . . ∧ Γ (An ) → Γ (B) is valid. Let d(Γ ( )) > 0, then Γ ( ) = ∆, [C : Σ( )].
By inductive hypothesis, we have that Σ(A1 )∧. . .∧Σ(An ) → Σ(B) is valid. By (RCK),
we obtain that also (C ⇒ Σ(A1 ))∧. . .∧(C ⇒ Σ(An )) → (C ⇒ Σ(B)) is valid. Then,
we get that (Λ ∨ (C ⇒ Σ(A1 ))) ∧ . . . ∧ (Λ ∨ (C ⇒ Σ(An ))) → (Λ ∨ (C ⇒ Σ(B)))
is also valid, that is Γ (A1 ) ∧ . . . ∧ Γ (An ) → Γ (B) is valid.
54 Nicola Olivetti and Gian Luca Pozzato
Now we can prove the soundness of the calculi, namely if Γ is derivable in N S,
then Γ is valid. By induction on the height of the derivation of Γ . In the base case, Γ is
an axiom, that is Γ = Γ (P, ¬P ); then, trivially P ∨ ¬P is valid, then also Γ (P, ¬P )
is valid by the fact that nested inference is sound. Similarly for Γ (>) and Γ (¬⊥). For
the inductive step, in order to save space, we only show the most interesting case of
(⇒− ): Γ = Γ (¬(A ⇒ B), [A0 : ∆]) is derived from (i) Γ (¬(A ⇒ B), [A0 : ∆, ¬B]),
(ii) ¬A, A0 , (iii) ¬A0 , A. By inductive hypothesis we have that A ↔ A0 is valid. We
show that also (∗) [¬(A ⇒ B) ∨ (A0 ⇒ (∆ ∨ ¬B))] → [¬(A ⇒ B) ∨ (A0 ⇒
∆)] is valid, then we conclude since nested inference is sound and by applying the
inductive hypothesis. To prove (*), by (RCK) we have that the following is valid:
[(A0 ⇒ B) ∧ (A0 ⇒ (∆ ∨ ¬B))] → (A0 ⇒ ∆). Since A ↔ A0 is valid, by (RCEA)
we get that (A ⇒ B) → (A0 ⇒ B) is valid, so that also (A ⇒ B) → ((A0 ⇒
(∆ ∨ ¬B)) → (A0 ⇒ ∆)) is valid, then we conclude by propositional reasoning.
(Completeness): If Γ is valid, then Γ has a derivation in N S. First of all, it can be
shown that weakening and contraction are height-preserving admissible in N S, that is
to say: (weakening) if Γ (∆) is derivable in N S with a derivation of height h, then also
Γ (∆, Σ) is derivable in N S with a proof of height h0 ≤ h, where ∆ and Σ are nested
sequents; (contraction) given a nested sequent ∆, if Γ (∆, ∆) has a derivation of height
h, then also Γ (∆) has a derivation of height h0 ≤ h. Moreover, the derivation of the
contracted sequent Γ (∆) does not add any rule application to the initial derivation.
Completeness is an easy consequence of the admissibility of the following rule cut:
Γ (F ) Γ (¬F )
(cut)
Γ (∅)
where F is a formula. The standard proof of admissibility of cut proceeds by a double
induction over the complexity of F and the sum of the heights of the derivations of the
two premises of (cut), in the sense that we replace one cut by one or several cuts on
formulas of smaller complexity, or on sequents derived by shorter derivations. We only
show the case of systems without MP and CSO, reminding to [2] for all the other details.
However, in N S the standard proof does not work in the following case, in which the
cut formula F is a conditional formula A ⇒ B:
(1) Γ ([A : B], [A0 : ∆]) (2) Γ (¬(A ⇒ B), [A0 : ∆, ¬B]) A, ¬A0 A0 , ¬A
+
(⇒ ) (⇒− )
(3) Γ (A ⇒ B, [A0 : ∆]) Γ (¬(A ⇒ B), [A0 : ∆])
(cut)
Γ ([A0 : ∆])
Indeed, even if we apply the inductive hypothesis on the heights of the derivations of
the premises to cut (2) and (3), obtaining (modulo weakening, which is admissible) a
derivation of (20 ) Γ ([A0 : ∆, ¬B], [A0 : ∆]), we cannot apply the inductive hypothesis
on the complexity of the cut formula to (20 ) and (10 ) Γ ([A : ∆, B], [A0 : ∆]) (obtained
from (1) again by weakening). Such an application would be needed in order to obtain a
derivation of Γ ([A0 : ∆], [A0 : ∆]) and then to conclude Γ ([A0 : ∆]) since contraction is
admissible: indeed, the two contexts are different, we have [A0 : ∆, ¬B] in (20 ) whereas
we have [A : ∆, B] in (10 ).
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 55
In order to tackle this problem, we need to prove another property, namely that if A
and A0 are equivalent, if a sequent Γ ([A : ∆]) is derivable in N S, then also Γ ([A0 : ∆]),
obtained by replacing A with the equivalent formula A0 , is also derivable. In turn, we
need (cut) to prove this property, therefore we prove both the properties (admissibility
of (cut) and “substitution” of A with A0 ) by mutual induction, namely:
In N S, the following propositions hold:
– (A) If Γ (F ) and Γ (¬F ) are derivable, so is Γ (∅), i.e. (cut) is admissible in N S;
– (B) if (I) Γ ([A : ∆]), (II) A, ¬A0 and (III) A0 , ¬A are derivable, then Γ ([A0 : ∆]) is
derivable.
Let us first consider (A). We have the following cases:
– (at least) one of the premises of (cut) is an instance of the axioms. Suppose that the
left premise is an instance of (AX). In case it has the form Γ (P, ¬P, F ), then also
Γ (P, ¬P ) is an instance of (AX) and we are done. Otherwise, we have Γ (F, ¬F ).
In this case, the right premise of (cut) has the form Γ (¬F, ¬F ), whereas the
conclusion is Γ (¬F ): since contraction is admissible, we conclude that Γ (¬F ) is
derivable and we are done. The other cases are symmetric. The cases in which one
premise of (cut) is an instance of either (AX> ) or (AX⊥ ) are easy and left to the
reader;
– the last step of one of the two premises is obtained by a rule (R) in which F is not
the principal formula. This case is standard, we can permute (R) over the cut, i.e.
we cut the premise(s) of (R) and then we apply (R) to the result of cut.
– F is the principal formula in the last step of both derivations of the premises of the
cut inference. There are several subcases, to save space we only consider the above
mentioned case in which the standard proof does not work, where the derivation is
as follows:
(1) Γ (¬(A ⇒ B), [A0 : ∆, ¬B]) A, ¬A0 A0 , ¬A (2) Γ ([A : B], [A0 : ∆])
(⇒− ) (⇒+ )
Γ (¬(A ⇒ B), [A0 : ∆]) (3) Γ (A ⇒ B, [A0 : ∆])
(cut)
Γ ([A0 : ∆])
First of all, since we have proofs for A, ¬A0 and for A0 , ¬A and the complexity of A
is lower than the one of A ⇒ B, we can apply the inductive hypothesis for (B) to (2),
obtaining a derivation of (20 ) Γ ([A0 : B], [A0 : ∆]). Since weakening is admissible,
from (3) we obtain a derivation of at most the same height of (30 ) Γ (A ⇒ B, [A0 :
∆, ¬B]). We can then conclude as follows: we first apply the inductive hypothesis on
the height for (A) to cut (1) and (30 ), obtaining a derivation of (4) Γ ([A0 : ∆, ¬B]).
By weakening, we have also a derivation of (40 ) Γ ([A0 : ∆, ¬B], [A0 : ∆]). Again
by weakening, from (20 ) we obtain a derivation of (200 ) Γ ([A0 : ∆, B], [A0 : ∆]).
We then apply the inductive hypothesis on the complexity of the cut formula to
cut (200 ) and (40 ), obtaining a derivation of Γ ([A0 : ∆], [A0 : ∆]), from which we
conclude since contraction is admissible.
Concerning (B), we proceed by induction on the height h of the premise (I), as follows:
56 Nicola Olivetti and Gian Luca Pozzato
– Base case: Γ ([A : ∆]) is an instance of the axioms, that is to say either ∆ =
Λ(P, ¬P ) or ∆ = Λ(>) or ∆ = Λ(¬⊥): we immediately conclude that also
Γ ([A0 : ∆]) is an instance of the axioms, and we are done;
– Inductive step: we have to consider all possible rules ending (looking forward) the
derivation of Γ ([A : ∆]). We only show the most interesting case, when (⇒− ) is
applied by using [A : ∆] as principal formula. The derivation ends as follows:
(1) Γ (¬(C ⇒ D), [A : ∆, ¬D]) (2) C, ¬A (3) A, ¬C
(⇒− )
Γ (¬(C ⇒ D), [A : ∆])
We can apply the inductive hypothesis to (1) to obtain a derivation of (10 ) Γ (¬(C ⇒
D), [A0 : ∆, ¬D]). Since weakening is admissible, from (II) we obtain a derivation
of (II 0 ) C, A, ¬A0 , from (III) we obtain a derivation of (III 0 ) A0 , ¬A, ¬C. Again
by weakening, from (2) and (3) we obtain derivations of (20 ) C, ¬A, ¬A0 and
(30 ) A0 , A, ¬C, respectively. We apply the inductive hypothesis of (A) that is that
cut holds for the formula A (of a given complexity c) and conclude as follows:
(II 0 ) C, A, ¬A0 (III 0 ) A0 , ¬A, ¬C
(20 ) C, ¬A, ¬A0 (30 ) A0 , A, ¬C
(cut) (cut)
(10 ) Γ (¬(C ⇒ D), [A0 : ∆, ¬D]) C, ¬A0 A0 , ¬C
−
(⇒ )
Γ (¬(C ⇒ D), [A0 : ∆])
With the admissibility of cut at hand, we can easily conclude the proof of completeness
of N S by showing that the axioms are derivable and that the set of derivable formulas is
closed under (Modus Ponens), (RCEA), and (RCK). A derivation of an instance of ID
has been shown in Figure 2. A derivation of an instance of MP is as follows:
(AX) (AX)
¬(A ⇒ B), ¬A, B, A ¬(A ⇒ B), ¬A, B, ¬B
(MP )
¬(A ⇒ B), ¬A, B
+
(→ )
¬(A ⇒ B), A → B
(→+ )
(A ⇒ B) → (A → B)
Here is a derivation of an instance of CEM:
(AX) (AX) (AX)
[A : B, ¬B], [A : ¬B] A, ¬A ¬A, A
(CEM )
[A : B], [A : ¬B]
+
(⇒ )
[A : B], A ⇒ ¬B
(⇒+ )
A ⇒ B, A ⇒ ¬B
(∨+ )
(A ⇒ B) ∨ (A ⇒ ¬B)
For (Modus Ponens), we have to show that, if (1) A → B ad (2) A are derivable,
then also B is derivable. Since weakening is admissible, we have also derivations
for (10 ) A → B, B, ¬A and (20 ) A, B. Furthermore, observe that (3) A, B, ¬A and
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 57
(4) ¬B, B, ¬A are both instances of (AX). Since cut is admissible (statement A above),
the following derivation shows that B is derivable:
(3) A, B, ¬A (4) ¬B, B, ¬A
0
(→− )
(1 ) A → B, B, ¬A ¬(A → B), B, ¬A
(cut)
(20 ) A, B B, ¬A
(cut)
B
For (RCEA), we have to show that if A ↔ B is derivable, then also (A ⇒ C) ↔ (B ⇒
C) is derivable. As usual, A ↔ B is an abbreviation for (A → B) ∧ (B → A). Since
A ↔ B is derivable, and since (∧+ ) and (→+ ) are invertible, we have a derivation
for A → B, then for (1) ¬A, B, and for B → A, then for (2) A, ¬B. We derive
(A ⇒ C) → (B ⇒ C) (the other half is symmetric) as follows:
(AX)
¬(A ⇒ C), [B : C, ¬C] (1) ¬A, B (2) A, ¬B
(⇒− )
¬(A ⇒ C), [B : C]
(⇒+ )
¬(A ⇒ C), B ⇒ C
(→+ )
(A ⇒ C) → (B ⇒ C)
For (RCK), suppose that we have a derivation in N S of (A1 ∧ . . . ∧ An ) → B. Since
(→+ ) is invertible, we have also a derivation of B, ¬(A1 ∧ . . . ∧ An ). Since (∧− )
is also invertible, then we have a derivation of B, ¬A1 , . . . , ¬An and, by weakening,
of (1) ¬(C ⇒ A1 ), . . . , ¬(C ⇒ An ), [C : B, ¬A1 , ¬A2 , . . . , ¬An ], from which we
conclude as follows:
(1) ¬(C ⇒ A1 ), . . . , ¬(C ⇒ An ), [C : B, ¬A1 , ¬A2 , . . . , ¬An ]
.
.
.
(⇒− ) (AX) (AX)
¬(C ⇒ A1 ), . . . , ¬(C ⇒ An ), [C : B, ¬A1 , ¬A2 ] C, ¬C ¬C, C
(⇒− ) (AX) (AX)
¬(C ⇒ A1 ), . . . , ¬(C ⇒ An ), [C : B, ¬A1 ] C, ¬C ¬C, C
(⇒− )
¬(C ⇒ A1 ), . . . , ¬(C ⇒ An ), [C : B]
(∧− )
¬(C ⇒ A1 ∧ . . . ∧ C ⇒ An ), [C : B]
(⇒+ )
¬(C ⇒ A1 ∧ . . . ∧ C ⇒ An ), C ⇒ B
(→+ )
(C ⇒ A1 ∧ . . . ∧ C ⇒ An ) → (C ⇒ B)
As usual, in order to obtain a decision procedure for the conditional logics under consid-
eration, we have to control the application of the rules (⇒− )/(CSO), (MP ), (CEM ),
and (ID) that otherwise may be applied infinitely often in a backward proof search,
since their principal formula is copied into the respective premise(s). In detail, we obtain
a sound, complete and terminating calculus if we restrict the applications of these rules
as follows [1, 2]: (⇒− ) can be applied only once to each formula ¬(A ⇒ B) with a
58 Nicola Olivetti and Gian Luca Pozzato
context [A0 : ∆] in each branch - the same for (CSO) in the system CK+CSO+ID; (ID)
can be applied only once to each context [A : ∆] in each branch; (MP ) can be applied
only once to each formula ¬(A ⇒ B) in each branch. For systems with (CEM ), we
need a more complicated mechanism: due to space limitations, we refer to [1] for this
case. These results give a PS PACE decision procedure for their respective logics.
4 Design of NESCOND
In this section we present a Prolog implementation of the nested sequent calculi N S.
The program, called NESCOND (NESted sequent calculi for CONDitional logics), is
inspired by the “lean” methodology of leanTAP, even if it does not follow its style in a
rigorous manner. The program comprises a set of clauses, each one of which implements
a sequent rule or axiom of N S. The proof search is provided for free by the mere
depth-first search mechanism of Prolog, without any additional ad hoc mechanism.
NESCOND represents a nested sequent with a Prolog list of the form:
[F 1, F 2, ..., F m,[[A 1,Gamma 1],AppliedConditionals 1],
[[A 2,Gamma 2],AppliedConditionals 2], ..., [[A n,Gamma n],AppliedConditionals n]] ]
In detail, elements of a nested sequent can be either formulas F or contexts. A context is
represented by a pair [Context,AppliedConditionals] where:
– Context is also a pair of the form [F,Gamma], where F is a formula of L and
Gamma is a Prolog list representing a nested sequent;
– AppliedConditionals is a Prolog list [A 1=>B 1,A 2=>B 2,...,A k=>B k],
keeping track of the negated conditionals to which the rule (⇒− ) has been already
applied by using Context in the current branch. This is used in order to implement
the restriction on the application of the rule (⇒− ) in order to ensure termination.
Symbols > and ⊥ are represented by constants true and false, respectively, whereas
connectives ¬, ∧, ∨, →, and ⇒ are represented by !, ˆ, v, ->, and =>.
As an example, the Prolog list
[p, q, !(p => q), [[p, [q v !p, [[p,[p => r]],[]], !r]],[p => q]], [[q, [p, !p]],[]]]
represents the nested sequent
P, Q, ¬(P ⇒ Q), [P : Q ∨ ¬P, [P : P ⇒ R], ¬R], [Q : P, ¬P ].
Furthermore, the list [p => q] in the leftmost context is used to represent the fact that,
in a backward proof search, the rule (⇒− ) has already been applied to ¬(P ⇒ Q) by
using [P : Q ∨ ¬P, [P : P ⇒ R], ¬R].
Let us now discuss more in detail the implementation of NESCOND, starting from
the description of some auxiliary predicates, and then distinguishing among the different
conditional logics considered.
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 59
4.1 Auxiliary predicates
In order to manipulate formulas “inside” a sequent, NESCOND makes use of the three
following auxiliary predicates:
– deepMember(+Formulas,+NS) succeeds if and only if either (i) the nested
sequent NS representing a nested sequent Γ contains all the fomulas in the list
Formulas or (ii) there exists a context [[A,Delta],AppliedConditionals]
in NS such that deepMember(Formulas,Delta) succeeds, that is to say there
is a nested sequent occurring in NS containing all the formulas of Formulas.
– deepSelect(+Formulas,+NS,-NewNS) operates exactly as deepMember,
however it removes the formulas of the list Formulas by replacing them with a
placeholder hole; the output term NewNS matches the resulting sequent.
– fillTheHole(+NS,+Formulas,-NewNS) replaces the placeholder hole
in NS with the formulas in the list Formulas. The resulting sequent matches the
output term NewNS.
4.2 NESCOND for CK
The calculi N S are implemented by the predicate
prove(+NS,-ProofTree).
This predicate succeeds if and only if the nested sequent represented by the list NS is
derivable. When the predicate succeeds, then the output term ProofTree matches with
a representation of the derivation found by the prover, used in order to display the proof
tree. For instance, in order to prove that the formula (A ⇒ (B ∧ C)) → (A ⇒ B) is
valid in CK, one queries NESCOND with the goal: prove([(a => b ˆ c) ->
(a => b)],ProofTree). Each clause of the prove predicate implements an
axiom or rule of N S. To search a derivation of a nested sequent Γ , NESCOND proceeds
as follows. First of all, if Γ is an axiom, the goal will succeed immediately by using one
of the following clauses for the axioms:
prove(NS,tree(ax)):-deepMember([P,!P],NS),!.
prove(NS,tree(axt)):-deepMember([top],NS),!.
prove(NS,tree(axb)):-deepMember([!bot],NS),!.
implementing (AX), (AX> ) and (AX⊥ ), respectively. If Γ is not an instance of the
axioms, then the first applicable rule will be chosen, e.g. if a nested sequent in Γ contains
a formula A v B then the clause implementing the (∨+ ) rule will be chosen, and
NESCOND will be recursively invoked on the unique premise of (∨+ ). NESCOND
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 (⇒− ) is as follows:
1. prove(NS,tree(condn,A,B,Sub1,Sub2,Sub3)):-
2. deepSelect([!(A => B),[[C,Delta],AppliedConditionals]],
NS,NewNS),
60 Nicola Olivetti and Gian Luca Pozzato
3. \+member(!(A => B),AppliedConditionals),!,
4. prove([A,!C],Sub2),
5. prove([C,!A],Sub3),
6. fillTheHole(NewNS,[!(A => B),
[[C,[!B|Delta]],[!(A => B)|AppliedConditionals]]],DefNS),
7. prove(DefNS,Sub1).
In line 2, the auxiliary predicate deepSelect is invoked in order to find both a
negated conditional ¬(A ⇒ B) and a context [C : ∆] in the sequent (even in a
nested subsequent). In this case, such formulas are replaced by the placeholder hole.
Line 3 implements the restriction on the application of (⇒− ) in order to guaran-
tee termination: the rule is applied only if ¬(A ⇒ B) does not belong to the list
AppliedConditionals of the selected context. Since the rules of N S are in-
vertible4 , a cut ! is introduced in order to avoid useless backtrackings in the choice
of the rule to apply. In lines 4, 5 and 7, NESCOND is recursively invoked on the
three premises of the rule. In line 7, NESCOND is invoked on the premise in which
the context [C : ∆] is replaced by [C : ∆, ¬B]. To this aim, in line 6 the auxil-
iary predicate fillTheHole(+NewNS,+Formulas,-DefNS) is invoked to re-
place the hole in NewNS, introduced by deepSelect, with the negated conditional
¬(A ⇒ B), which is copied into the premise, and the context [C : ∆, ¬B], whose list
of AppliedConditionals is updated by adding the formula ¬(A ⇒ B) itself.
4.3 NESCOND for extensions of CK
The implementation of the calculi for extensions of CK with axioms ID and MP are very
similar. For systems allowing ID, contexts are triples [Context, AppliedConditionals,
AllowID]. The third element AllowID is a flag used in order to implement the re-
striction on the application of the rule (ID), namely the rule is applied to a context only
if AllowID=true:
prove(NS,tree(id,A,SubTree)):-
deepSelect([[[A,Delta],AppliedConditionals,true]]],NS,NewNS),!,
fillTheHole(NewNS,[[[A,[!A|Delta]],AppliedConditionals,false]]],DefNS),
prove(DefNS,SubTree).
When (ID) is applied to [Context, AppliedConditionals, true] then the
predicate prove is invoked on the unique premise of the rule DefNS, and the flag is
set to false in order to avoid multiple applications in a backward proof search.
The restriction on the application of the rule (MP ) is implemented by equipping the
predicate prove by a third argument, AppliedMP, a Prolog list keeping track of the
negated conditionals to which the rule has already been applied in the current branch.
The clause of prove implementing (MP ) is as follows:
4
The rule (⇒− ), as well as (CEM ), are only “weakly” invertible, in the sense that only the
leftmost premise of these rules can be obtained by weakening from the respective conclusions
(see [2] for details).
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 61
1. prove(NS,AppliedMP,tree(mp,A,B,Sub1,Sub2)):-
2. deepSelect([!(A => B)],NS,NewNS),
3. \+member(A => B,AppliedMP),!,
4. fillTheHole(NewNS,[A,!(A => B)],NS1),
5. fillTheHole(NewNS,[!B,!(A => B)],NS2),
6. prove(NS1,[A => B|AppliedMP],Sub1),
7. prove(NS2,[A => B|AppliedMP],Sub2).
The rule is applicable to a formula ¬(A ⇒ B) only if [A => B] does not be-
long to AppliedMP (line 3). When (MP ) is applied, then [A => B] is added to
AppliedMP in the recursive calls of prove on the premises of the rule (lines 6 and 7).
The implemetation of the calculus for the flat fragment of CK+CSO+ID, correspond-
ing to KLM cumulative logic C, is very similar to the one for CK+ID; the only difference
is that the rule (⇒− ) is replaced by (CSO). This does not make use of the predicate
deepSelect to “look inside” a sequent to find the principal formulas ¬(A ⇒ B)
and [C : ∆]: since the calculus only deals with the flat fragment of the logic under
consideration, such principal formulas are directly selected from the current sequent
by easy membership tests (standard Prolog predicates member and select), without
searching inside other contexts.
As mentioned, NESCOND also deals with extensions with CEM; the clause imple-
menting the rule (CEM ) is as follows:
1. prove(NS,tree(cem,A,B,Sub1,Sub2,Sub3)):-
2. deepSelect([[[A,Delta],ApplCond1],[[B,Sigma],ApplCond2]],
NS,NewNS),
3. notSequentIncluded(Delta,Sigma),!,
4. prove([A,!B],Sub2),
5. prove([B,!A],Sub3),
6. append(Delta,Sigma,ResDelta),
7. fillTheHole(NewNS,[[[A,ResDelta],ApplCond1],
[[B,Sigma],ApplCond2]],DefNS),
8. prove(DefNS,Sub1).
In line 3 the predicate notSequentIncluded is invoked: this predicate implements
the restriction on the application of the rule described in the previous section in order to
ensure termination.
5 Performances of NESCOND
The performances of NESCOND are promising. We have tested it by running SICStus
Prolog 4.0.2 on an Apple MacBook Pro, 3.06 GHz Intel Core 2 Duo, 4GB RAM machine.
We have performed two kind of tests:
– we have compared the performances of NESCOND for CK with the ones of two other
provers for conditional logics, namely CondLean, implementing labelled sequent
calculi [17, 18], and the goal-directed procedure G OAL DUCK [19]. To this aim, we
have tested the three theorem provers on randomly generated sequents, obtaining the
62 Nicola Olivetti and Gian Luca Pozzato
results shown in Figure 3. It is easy to conclude that the performances of NESCOND
are better in all cases: in particular, concerning sequents containing formulas with a
high level of conditional nesting (15), with a 1ms time limit, G OAL DUCK is not able
to answer in the 41% of cases, whereas CondLean finds all the valid sequents but it
is not able to find any non-valid ones. NESCOND answers correctly for the 100%
of the generated formulas, discovering that all the missing answers of CondLean are
non-valid ones;
– we have tested NESCOND over a set of 88 CK valid formulas obtained by translating
K valid formulas5 provided by Heuerding and used to test the theorem prover
ModLeanTAP [5] by Beckert and Goré. Also in this case, the results, shown in
Figure 4, are encouraging: NESCOND is not able to give an answer in less than 1
ms only in 16 cases over 88; the number of timeouts drops to 7 if we extend the time
limit to 5 seconds.
number of formulas : 30 Prop. vars: 5 Depth: 3 Timeout: 1 ms number of formulas: 10 Prop. vars: 3 Depth: 15 Timeout: 1ms
yes no timeout yes no timeout
UCK 73,00% 21,00% 6,00% UCK 55,00% 4,00% 41,00%
CondLean 74,00% 0,00% 26,00% CondLean 69,00% 0,00% 31,00%
Nested sequents 74,00% 26,00% 0,00% Nested sequents 69,00% 31,00% 0,00%
Fig. 3. NESCOND vs CondLean vs G OAL DUCK
Time limit (ms) 1 100 1000 5000 30000
NESCOND 16 13 10 7 5
CondLean 22 16 14 10 9
Fig. 4. Number of timeouts of NESCOND and CondLean over 88 CK valid formulas.
Time limit (ms) 1 50 100 5000
Percentage of timeouts 30% 28% 27% 20%
Fig. 5. Percentage of timeouts of NESCOND for extensions of CK.
These results show that the performances of NESCOND are encouraging, probably
better than the ones of the other existing provers for conditional logics (we are cur-
rently completing the comparative statistics). Figure 5 shows that this also holds for
extensions of CK: in the 70% of the tests (all of them are valid formulas), NESCOND
gives an answer in less than 1ms. The remaining 30% concerns the case of CEM(+ID),
where the performances worsen because of the overhead of the termination mechanism.
We note in passim that it does not exist a set of acknowledged benchmarks for condi-
tional logics. We are currently building a set of meaningful tests, they can be found at
http://www.di.unito.it/∼pozzato/nescond/.
6 Conclusions and Future Issues
In this work we have presented NESCOND, a theorem prover for conditional logics
implementing nested sequent calculi introduced in [1]. The performances described in
the previous section show that nested sequent calculi do not only provide elegant and
5
A is replaced by > ⇒ A, whereas A is replaced by ¬(> ⇒ ¬A).
Nested Sequent Calculi and Theorem Proving for Normal Conditional Logics 63
natural calculi for conditional logics, but they are also significant for developing efficient
theorem provers for them. In future research we aim to extend NESCOND to other
systems of conditional logics. To this regard, we strongly conjecture that adding a rule
for (CS) will be enough to cover the whole cube of the extensions of CK generated by
axioms (ID), (MP), (CEM) and (CS). This will be object of subsequent research.
References
1. Alenda, R., Olivetti, N., Pozzato, G.L.: Nested Sequent Calculi for Conditional Logics. In:
Luis Fariñas del Cerro, Andreas Herzig, J.M. (ed.) Logics in Artificial Intelligence - 13th
European Conference, JELIA 2012. Lecture Notes in Artificial Intelligence (LNAI), vol. 7519,
pp. 14–27. Springer-Verlag, Toulouse, France (Sptember 2012)
2. Alenda, R., Olivetti, N., Pozzato, G.L.: Nested Sequents Calculi for Normal Conditional
Logics. Journal of Logic and Computation to appear, 1–48 (2013)
3. Baltag, A., Smets, S.: The logic of conditional doxastic actions. Texts in Logic and Games,
Special Issue on New Perspectives on Games and Interaction 4, 9–31 (2008)
4. Beckert, B., Posegga, J.: leanTAP: Lean tableau-based deduction. Journal of Automated
Reasoning 15(3), 339–358 (1995)
5. Beckert, B., Goré, R.: Free variable tableaux for propositional modal logics. In: Proceedings
of Tableaux 97. LNCS, vol. 1227, pp. 91–106. Springer, Pont-a-Mousson, France (1997)
6. Board, O.: Dynamic interactive epistemology. Games and Economic Behavior 49(1), 49–80
(2004)
7. Boutilier, C.: Conditional logics of normality: a modal approach. Artificial Intelligence 68(1),
87–154 (1994)
8. Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: A conditional constructive logic for
access control and its sequent calculus. In: Brünnler, K., Metcalfe, G. (eds.) Tableaux 2011.
Lecture Notes in Artificial Intelligence (LNAI), vol. 6793, pp. 164–179. Springer-Verlag,
Bern, Switzerland (July 2011)
9. Genovese, V., Giordano, L., Gliozzi, V., Pozzato, G.L.: Logics in access control: A conditional
approach. Journal of Logic and Computation p. to appear (2012)
10. Ginsberg, M.L.: Counterfactuals. Artificial Intelligence 30(1), 35–79 (1986)
11. Giordano, L., Gliozzi, V., Olivetti, N.: Weak AGM postulates and strong ramsey test: A logical
formalization. Artificial Intelligence 168(1-2), 1–37 (2005)
12. Grahne, G.: Updates and counterfactuals. Journal of Logic and Computation 8(1), 87–117
(1998)
13. Kashima, R.: Cut-free sequent calculi for some tense logics. Studia Logica 53(1), 119–136
(1994)
14. Kraus, S., Lehmann, D., Magidor, M.: Nonmonotonic reasoning, preferential models and
cumulative logics. Artificial Intelligence 44(1-2), 167–207 (1990)
15. Lewis, D.: Counterfactuals. Basil Blackwell Ltd (1973)
16. Nute, D.: Topics in conditional logic. Reidel, Dordrecht (1980)
17. Olivetti, N., Pozzato, G.L.: CondLean: A Theorem Prover for Conditional Logics. In:
Cialdea Meyer, M., Pirri, F. (eds.) Tableaux 2003. LNAI, vol. 2796, pp. 264–270. Springer,
Roma, Italy (September 2003)
18. Olivetti, N., Pozzato, G.L.: CondLean 3.0: Improving Condlean for Stronger Conditional
Logics. In: Beckert, B. (ed.) Proceedings of Tableaux 2005. LNAI, vol. 3702, pp. 328–332.
Springer-Verlag, Koblenz, Germany (September 2005)
19. Olivetti, N., Pozzato, G.L.: Theorem Proving for Conditional Logics: CondLean and Goal-
Duck. Journal of Applied Non-Classical Logics (JANCL) 18(4), 427–473 (2008)
20. Olivetti, N., Pozzato, G.L., Schwind, C.B.: A Sequent Calculus and a Theorem Prover for
Standard Conditional Logics. ACM Transactions on Computational Logic (ToCL) 8(4) (2007)