In this paper we focus on proof methods and theorem proving for normal conditional logics, by describing nested sequent calculi as well as a theorem prover for them. Nested sequent calculi are a useful generalization of ordinary sequent 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 CONDitional 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/
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. 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, conditional 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 PSPACE 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 CONP). For flat CK+CSO+ID = cumulative logic C we also get a PSPACE 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 PSPACE 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 GOALDU CK [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.
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 ID CEM MP CSO
Axiom A ⇒ A (A ⇒ B) ∨ (A ⇒ ¬B) (A ⇒ B) → (A → B) (A ⇒ B)∧(B ⇒ A) → ((A ⇒ C) → (B ⇒ C))
Model condition f(w, [A]) ⊆ [A] | f(w, [A]) |≤ 1 w ∈ [A] implies w ∈ f(w, [A]) f(w, [A]) ⊆ [B] and f(w, [B]) ⊆ [A] implies 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 Γ( P, ¬ P ) ( AX )
P ∈ TMA Γ( A ) Γ( A ∧ B )
Γ( B ) ( ∧+ ) Γ( ¬ A, B ) Γ( A → B ) ( →+ ) Γ([ A : B ]) Γ( A ⇒ B ) ( ⇒+ ) Γ([ A : Δ, ¬ A ]) ( ID ) Γ([ A : Δ])
Γ( ⊤) ( AX ⊤) Γ( ¬ A, ¬ B ) Γ( ¬ ( A ∧ B ) ( ∧−) Γ( ¬ ⊥) ( AX ⊥)
Γ( Γ¬( A A ) ) ( ¬ ) Γ( A, B ) Γ( A ∨ B ) ( ∨+ ) Γ( ¬ A ) Γ( ¬ B ) Γ( ¬ ( A ∨ B ) ( ∨−) Γ( A ) Γ( ¬ B ) ( →−) Γ( ¬ ( A → B ) Γ( ¬ ( A ⇒ B ) , [ A ′ : Δ, ¬ B ])
,A ¬ A ′ A ′, ¬ A ( ⇒−) Γ( ¬ ( A ⇒ B ) , [ A ′ : Δ]) Γ( ¬ ( A ⇒ B ) , A ) Γ( ¬ ( A ⇒ B ) , ¬ B ) ( MP ) Γ( ¬ ( A ⇒ B ) Γ([ A : Δ, Σ] , [ B : Σ]) A, ¬ B B, ¬ A ( CEM Γ([ A : Δ] , [ B : Σ]) ) Γ, ¬ ( A ⇒ B ) , [ A ′ : Δ, ¬ B ] Γ, ¬ ( A ⇒ B ) , [ A : A ′] Γ, ¬ ( A ⇒ B ) , [ A ′ : A ]
( CSO ) Γ, ¬ ( A ⇒ B ) , [ A ′ : Δ] 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. P ⇒ P (AX) (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.
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:
(
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:
(
Concerning (B), we proceed by induction on the height h of the premise (I), as follows:
– 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:
(
(
C, ¬A0 (cut) (III0) A0, ¬A, ¬C (30) A0, A, ¬C
A0, ¬C (⇒−) (cut) 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: Here is a derivation of an instance of CEM:
(AX) ¬(A ⇒ B), ¬A, B, A ¬(A ⇒ B), ¬A, B, ¬B (AX) (MP ) ¬(A ⇒ B), ¬A, B ¬(A ⇒ B), A → B (A ⇒ B) → (A → B) (→+)
(→+) [A : B, ¬B], [A : ¬B]
A, ¬A (AX) (AX) ¬A, A (AX) (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 (
B
B, ¬A
(cut)
(
¬(A → B), B, ¬A
(
(AX)
¬(A ⇒ C), [B : C, ¬C]
(
(
... ¬(C ⇒ A1), . . . , ¬(C ⇒ An), [C : B, ¬A1, ¬A2] ¬(C ⇒ A1), . . . , ¬(C ⇒ An), [C : B, ¬A1] (⇒−)
(AX) 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) (AX) (⇒−) (∧−) (⇒+) (→+)
(AX) C, ¬C ¬C, C (AX) (⇒−) As usual, in order to obtain a decision procedure for the conditional logics under consideration, 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 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 PSPACE decision procedure for their respective logics. 4
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: 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.
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.
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), \+member(!(A => B),AppliedConditionals),!, prove([A,!C],Sub2), prove([C,!A],Sub3), fillTheHole(NewNS,[!(A => B),
[[C,[!B|Delta]],[!(A => B)|AppliedConditionals]]],DefNS), 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 guarantee 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 invertible4, 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 auxiliary predicate fillTheHole(+NewNS,+Formulas,-DefNS) is invoked to replace 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.
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 restriction 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). 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 belong 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, corresponding 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 implementing 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. 4. 5. 6. 7. 8.
notSequentIncluded(Delta,Sigma),!, prove([A,!B],Sub2), prove([B,!A],Sub3), append(Delta,Sigma,ResDelta), fillTheHole(NewNS,[[[A,ResDelta],ApplCond1],
[[B,Sigma],ApplCond2]],DefNS), 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.
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 GOALDUCK [19]. To this aim, we
have tested the three theorem provers on randomly generated sequents, obtaining the
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 (
yes UCK 73,00% CondLean 74,00% Nested sequents 74,00%
Depth: 3
no 21,00% 0,00% 26,00%
Timeout: 1 ms timeout 6,00% 26,00% 0,00% number of formulas: 10 Prop. vars: 3
yes UCK 55,00% CondLean 69,00% Nested sequents 69,00%
Depth: 15 no 4,00% 0,00% 31,00%
Fig. 3. NESCOND vs CondLean vs GOALDU CK Time limit (ms)
NESCOND CondLean 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 currently 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 conditional logics. We are currently building a set of meaningful tests, they can be found at http://www.di.unito.it/∼pozzato/nescond/. 6
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
A is replaced by > ⇒ A, whereas A is replaced by ¬(> ⇒ ¬A). 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.