Transcript Slides presented at TABLEAUX 2005

CondLean 3.0: improving CondLean
for stronger Conditional Logics
Nicola Olivetti – Gian Luca Pozzato
Dipartimento di Informatica - Università degli studi di Torino
Outline
• Brief introduction of Conditional Logics
• Sequent calculi SeqS for some standard conditional
logics
• List of results, in order to obtain a decision procedure
for conditional logics
• CondLean 3.0: a SICStus Prolog implementation of
sequent calculi SeqS
• Conclusions, future work and references
1
Conditional logics
Conditional logics
• Conditional logics have a long history
• Recently, they have been used in some branches of
artificial intelligence, such as:
non-monotonic reasoning (for example, prototypical
reasoning and default reasoning);
belief revision;
deductive databases;
representation of counterfactuals.
Conditional logics
Syntax
• Conditional logic is an extension of classical logic by the
conditional operator .
• We consider a language L over a set ATM of
propositional variables. Formulas of L are obtained applying
the classical connectives and the conditional operator  to
the propositional variables.
Conditional logics
Semantics
• We consider the selection function semantics; the model
is a triple:
< W, f, [ ] >
- W is a non-empty set of items called worlds;
- f is a function f: W x 2W  2W , called the selection function;
- [ ] is an evaluation function [ ] : ATM  2W.
Conditional logics
Semantics
• The selection function f (w, [A]) selects the worlds “closest”
to w given the information A.
Conditional logics
Semantics
• [ ] assigns to an atomic formula P the set of worlds where P
is true; [ ] is also extended to complex formulas as follows :
[]=
[ A  B ] = (W - [ A ])  [ B ]
[ A  B ] = {w  W | f (w, [ A ])  [ B ]}
• A conditional formula A  B is true in a world w if B is true
in all the worlds “closest” to w given the information A.
Conditional logics
Semantics
• We say that a formula A is valid in a model M if [ A ] = W. A
formula A is valid if it is valid in every model M.
Conditional logics
System CK
• The semantics above characterizes the minimal normal
conditional logic CK, which is axiomatized as follows:
Conditional logics - System CK
All the tautologies of the classical propositional logic
are CK axioms;
modus ponens:
AB
A
B
AB
RCEA:
RCK:
(A  C)  (B  C)
(A1  A2  …  An)  B
(C  A1  C  A2  …  C  An)  (C  B)
Conditional logics
Extensions of CK
With some properties of the selection function, we have the
following extensions:
System
Axiom
Selection function property
CK+ID
CK+MP
CK+CS
AA
(A  B)  (A  B)
f (x, [ A ])  [ A ]
w  [ A ]  w  f (w, [ A ])
w  [ A ]  f (w, [ A ])  {w}
CK+CEM
(A  B)  (A  B)
(A B)  (A  B)
| f (w, [ A ]) |  1
2
Sequent Calculi SeqS
Sequent Calculi SeqS
• In [OlivettiSchwind01], [OlivettiPozzatoSchwind05]
sequent calculi for conditional logics, called SeqS, are
introduced.
• SeqS consider CK and extensions CK+{ID, MP, CS,
CEM} and all the combinations of them, except for those
combining both CEM and MP
• These calculi use transition formulas and labels, in a
similar way to [Viganò00] and [Gabbay96].
Sequent Calculi SeqS
• A sequent is a pair < ,  >, written as usual as 
;
 and  are multisets of labelled formulas; we have two
kinds of formulas:
world formulas, like x: A;
transition formulas, like x A y .
• A world formula x: A represents that the formula A is
true in the world x.
• A transition formula x A y represents that y  f (x, [A]).
Sequent Calculi SeqS
SeqCK:
Sequent Calculi SeqS
Rules for the extensions of CK:
Theorem (soundness and completeness of SeqS): 
valid iff it is derivable in SeqS.
 is
3
How to obtain a
decision procedure
How to obtain a decision procedure
• SeqS calculi have the following rules:
(L)
(CEM)
, x: A  B
, x
A
, x: A  B, y: B
y
, x: A  B
, x A y
, x A z
A
y
, x

(, x A y


)[y,z/u]
How to obtain a decision procedure
• In backward proof search, the above rules add a formula
in the premise (i.e. they copy their principal formula in their
premises)
• In order to obtain a decision procedure, it is essential to
control the application of these rules.
How to obtain a decision procedure
• In [OlivettiPozzatoSchwind05 : submitted] it is shown
that:
1. one needs to apply (L) at most once on the same
formula x: A  B by using the same transition x A y
2. one needs to apply (L) by using
C
x=y or x
y
x
A
y only when
3. the same restrictions on the applications of (CEM)
How to obtain a decision procedure
• SeqCK and SeqID are complete even if we reformulate
(L) as follows:
(L)
x
C
y
x
x
C
A
y
y, , x: A  B
x

C
y, , y: B

4
Design of
CondLean 3.0
Design of CondLean 3.0
• CondLean 3.0 is a Prolog implementation of SeqS calculi;
it is written in SICStus Prolog and it is inspired by leanTAP,
introduced in [BeckertPosegga96].
• The program comprises a set of clauses, each one of
them represents a sequent rule or axiom; the proof search is
provided for free by the mere depth-first search mechanism
of Prolog.
Design of CondLean 3.0
• CondLean 3.0 vs CondLean:
1. CondLean is a t.p. for CK and its extensions MP, ID,
and MP+ID, whereas CondLean 3.0 includes extensions CS
and CEM and all combinations of ID, MP, CS, and CEM,
except those combining both CEM and MP
2. CondLean implements sequent calculi with explicit
contractions, whereas CondLean 3.0 implements SeqS as in
[OlivettiPozzatoSchwind05], where the crucial rule (L) is
invertible
Design of CondLean 3.0
• The sequent calculi are implemented by the predicate
prove(Cond, Sigma, Delta, Labels)
• This predicate succeeds if and only if the sequent 
is derivable in SeqS, where

- Sigma e Delta are the lists representing multisets  and 
- Labels is the list of labels introduced in that branch
- Cond is a list of pairs [F, Used], where F is a conditional
formula and Used the list of transitions already used to
apply (L) on F
Design of CondLean 3.0
•Each clause of predicate prove implements one axiom or
rule of SeqS.
• The clauses of prove are ordered to postpone the
application of the branching rules.
Example 1: clause implementing (AX) axiom; both the
antecedent and the consequent contain the same complex
formula F:
(AX)
, F
, F
prove(_[_,_,ComplexSigma],[_,_,ComplexDelta],_):member(F,ComplexSigma),
member(F,ComplexDelta),!.
Design of CondLean 3.0
Example 2: clause implementing (R):
(R)
, x

A
y
, y: B
, x: A  B
prove(Cond,[LitSigma,TransSigma,ComplexSigma],
[LitDelta,TransDelta,ComplexDelta],Labels):
select([X,A => B],ComplexDelta,ResComplexDelta),!,
createLabels(Y,Labels),
put([Y,B], LitDelta, ResComplexDelta,
NewLitDelta, NewComplexDelta),
prove(Cond,[LitSigma, [[X,A,Y]|TransSigma],
ComplexSigma],[NewLitDelta,TransDelta,
NewComplexDelta],[Y|Labels]).
Design of CondLean 3.0
Example 3: clause implementing (L):
(L)
, x: A  B
, x A y
, x: A  B
, x: A  B, y: B

prove(Cond,[LitSigma,TransSigma,ComplexSigma],
[LitDelta,TransDelta,ComplexDelta],Labels):
member([X,A => B],ComplexSigma),
select([[X,A => B],Used],Cond,TempCond),
member([X,C,Y],TransSigma),
\+member([X,C,Y],Used),!,
put([Y,B], LitSigma, ComplexSigma,
NewLitSigma, NewComplexSigma),
…

Design of CondLean 3.0
Example 3: clause implementing (L):
(L)
, x: A  B
, x A y
, x: A  B
, x: A  B, y: B


prove(Cond,[LitSigma,TransSigma,ComplexSigma],
[LitDelta,TransDelta,ComplexDelta],Labels):
…
prove([[[X,A=>B],[[X,C,Y]|Used]]|TempCond],
[LitSigma,TransSigma,ComplexSigma],
[LitDelta,[X,A,Y]|TransDelta],ComplexDelta],Labels),
prove([[[X,A=>B],[[X,C,Y]|Used]]|TempCond],
[NewLitSigma,TransSigma,NewComplexSigma],
[LitDelta,TransDelta,ComplexDelta],Labels).
Design of CondLean 3.0
• For systems allowing (CEM) another parameter Tr is
added to the predicate prove:
prove(Tr, Cond, Sigma, Delta, Labels)
• It is a list of pairs [T,Used] where T is a transition
formula and Used the list of transitions already used to
apply (CEM) on T
• The application of (CEM) is restricted as in the case of
(L)
Design of CondLean 3.0
• We present three different implmentations for our
theorem provers:
1. Constant labels version (for all the systems)
2. Free-variables version
3. Heuristic version
} (only for SeqCK and SeqID)
Design of CondLean 3.0
1. Constant labels version
• This version makes use of Prolog constants to represent
SeqS’s labels, introdouced by the (R) rule.
• In SeqCK and SeqID…
Design of CondLean 3.0
• When the (L) clause is used to prove  , a
backtracking point is introduced by the choice of a label y
occurring in the two premises:
(L)

, x
A
, y: B
y
, x: A  B


• If there are n labels to choose, the computation might
succeed only after n-1 backtracking steps, with a significant loss
of efficiency.
Design of CondLean 3.0
2. Free-variables version
• In this implementation, CondLean 3.0 makes use of
Prolog variables to represent all the labels that can be used
in an application of the (L) clause.
• This solution is inspired to the free-variable tableaux
introduced in [BeckertGorè97].
Design of CondLean 3.0
Free variable
(L)

, x
A
, V: B
V
, x: A  B


Each free variable will be then istantiated by Prolog’s pattern
matching either to apply the (EQ) rule, or to close a branch
with an axiom.
Design of CondLean 3.0
• To manage free variable domains we use the constraints
(CLP); when a free variable V is introduced by the
application of (L), a constraint on its domain is added to
the constraint store.
• The constraint solver (given for free by the clpfd library of
SICStus Prolog) will control the consistency of the constraint
store during the computation in a very efficient way.
Design of CondLean 3.0
3. Heuristic version
• This implementation performs a “two-phase”
computation:
1. An incomplete theorem prover searches a derivation
exploring a reduced search space, to check the validity of a
sequent in a very small time;
2. In case of failure of phase 1, the free variable version is
called to complete the computation.
• On a valid sequent with over 120 connectives, the
heuristic version succeeds in 460 msec versus 4326 msec of
the free variable version.
Design of CondLean 3.0
• The performances of the three versions are promising.
• We have tested CondLean 3.0 - free variable version – for
SeqCK obtaining the following results; we define the
sequent degree as the maximum level of nesting of the
conditional operator.
Sequent degree
Time to succeed (ms)
2
5
6
500
9
11
15
650 1000 2000
• One can download the source code and the application
CondLean 3.0 at the following address:
www.di.unito.it/~pozzato/CondLean 3.0
5
Conclusion and
Future work
Conclusions and Future
work
• To the best of our knowldege, CondLean 3.0 is the first
theorem prover for CK and extensions with ID, MP, CEM,
and CS.
•We are working on extending CondLean to other
conditional systems (AC, CV, …)
• We intend to develop free variable and heuristic versions
for systems with MP, CS, and CEM
6
References
References
[BeckertGorè97] Bernard Beckert and Rajeev Gorè. Free Variable
Tableaux for Propositional Modal Logics. Tableaux-97, LNCS 1227,
Springer, pp. 91-106.
[BeckertPosegga96] Bernard Beckert and Joachim Posegga. leanTAP:
Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3),
pp. 339-358.
[Gabbay96] Dov. M. Gabbay. Labelled deductive systems (vol. i). Oxford
logic guides, Oxford University Press.
References
[OlivettiPozzato03] Nicola Olivetti and Gian Luca Pozzato. CondLean: A
Theorem Prover for Conditional Logics. In Proc. of TABLEAUX 2003
(Automated Reasoning with Analytic Tableaux and Related Methods),
volume 2796 of LNAI, Springer, pp. 264-270.
[OlivettiPozzatoSchwind05] Nicola Olivetti, Gian Luca Pozzato and
Camilla B. Schwind. A Sequent Calculus and a Theorem Prover for
Standard Conditional Logics: Extended version. Technical Report 87/05,
Dipartimento di Informatica, Università degli Studi di Torino, Italy, 2005.
References
[Pozzato03] Gian Luca Pozzato. Deduzione Automatica per Logiche
Condizionali: Analisi e Sviluppo di un Theorem Prover. Tesi di laurea,
Informatica, Università di Torino. In Italian, download at
http://www.di.unito.it/~pozzato/tesiPozzato.html
[OlivettiSchwind01] Nicola Olivetti and Camilla B. Schwind. A Calculus
and Complexity Bound for Minimal Conditional Logic. Proc. ICTCS01 Italian Conference on Theoretical Computer Science, vol. LNCS 2202, pp.
384-404.
[Viganò00] Luca Viganò. Labelled Non-classical Logics. Kluwer
Academic Publishers, Dordrecht.