Transcript Slides presented at UNILOG 2005

CondLean 2.0: a Theorem Prover for
standard 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 and the reformulation BSeqS
• CondLean 2.0: a SICStus Prolog implementation of sequent
calculi BSeqS
• 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:
Conditional logics
Semantics
• We consider the selection function semantics; the model is a triple:
< W, f, [ ] >
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;
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;
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
Systems CK{+MP}{+ID}
With some properties of the selection function, we have the following
extensions:
System
Axiom
Selection function property
Conditional logics
Systems CK{+MP}{+ID}
With some properties of the selection function, we have the following
extensions:
System
Axiom
Selection function property
CK+ID
AA
f (x, [ A ])  [ A ]
Conditional logics
Systems CK{+MP}{+ID}
With some properties of the selection function, we have the following
extensions:
System
CK+ID
CK+MP
Axiom
AA
(A  B)  (A  B)
Selection function property
f (x, [ A ])  [ A ]
w  [ A ]  w  f (w, [ A ])
Conditional logics
Systems CK{+MP}{+ID}
With some properties of the selection function, we have the following
extensions:
System
Axiom
Selection function property
CK+ID
CK+MP
AA
(A  B)  (A  B)
f (x, [ A ])  [ A ]
w  [ A ]  w  f (w, [ A ])
CK+MP+ID
(A  B)  (A  B)
AA
w  [ A ]  w  f (w, [ A ])
f (x, [ A ])  [ A ]
2
Sequent Calculi SeqS
Sequent Calculi SeqS
• In [OlivettiSchwind01] sequent calculi for conditional logics
CK{+MP}{+ID} called SeqS, where S={CK, ID, MP, ID+MP}, are
introduced.
• 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 formulas; we have two kinds of formulas:
Sequent Calculi SeqS
• A sequent is a pair < ,  >, written as usual as 
;
 and  are multisets of formulas; we have two kinds of formulas:
Labelled formulas, like x: A;
Sequent Calculi SeqS
• A sequent is a pair < ,  >, written as usual as 
;
 and  are multisets of formulas; we have two kinds of formulas:
Labelled formulas, like x: A;
transition formulas, like x
A
y .
Sequent Calculi SeqS
• A sequent is a pair < ,  >, written as usual as 
;
 and  are multisets of formulas; we have two kinds of formulas:
Labelled formulas, like x: A;
transition formulas, like x
A
y .
• A labelled formula x: A represents that the formula A is true in the
world x.
Sequent Calculi SeqS
• A sequent is a pair < ,  >, written as usual as 
;
 and  are multisets of formulas; we have two kinds of formulas:
Labelled formulas, like x: A;
transition formulas, like x
A
y .
• A labelled 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
Theorem (soundness and completeness of SeqS): 
it is derivable in SeqS.
 is valid iff
3
How to obtain a
decision procedure
How to obtain a decision procedure
• SeqS calculi have the following contraction rules:
(ContrR)


, F, F
, F
(ContrL)
, F, F
, F


How to obtain a decision procedure
• SeqS calculi have the following contraction rules:
(ContrR)


, F, F
, F
(ContrL)
, F, F
, F


• In backward proof search, the contraction rules add a formula in the
premise; all the other rules are analytic.
• In order to obtain a decision procedure, it is essential to control the
application of the contraction rules.
How to obtain a decision procedure
In [OlivettiSchwind01] it is shown that:
the contraction rules can be eliminated in SeqCK
SeqCK is complete without (ContrL) e (ContrR); so we have a decision
procedure for CK (all the SeqCK’s rules are analytic).
How to obtain a decision procedure
• In [Pozzato03] it is shown that:
How to obtain a decision procedure
• In [Pozzato03] it is shown that:
1. SeqID is complete without the contraction rules.
How to obtain a decision procedure
• In [Pozzato03] it is shown that:
1. SeqID is complete without the contraction rules.
2. SeqMP and SeqID+MP are NOT complete without the
contraction rules.
• This analysis is inspired by the work made by Luca Viganò for modal
logic T [Viganò00]
How to obtain a decision procedure
• One can control the application of the contraction rules as follows:
How to obtain a decision procedure
• One can control the application of the contraction rules as follows:
2.1. SeqMP and SeqID+MP are complete without the (ContrR)
rule.
How to obtain a decision procedure
• One can control the application of the contraction rules as follows:
2.1. SeqMP and SeqID+MP are complete without the (ContrR)
rule.
2.2. In SeqMP and SeqID+MP one needs to apply the (ContrL) rule
at most one time on every conditional formula x: A  B in every
branch of the proof tree.
• Here are the BSeqS calculi presented in [OlivettiPozzatoSchwind04]:
How to obtain a decision procedure
• The (L) rule is “split” in three rules, to keep into account of the
necessary application of (ContrL).
How to obtain a decision procedure
• The (L) rule is “split” in three rules, to keep into account of the
necessary application of (ContrL).
1. The first rule decomposes the principal formula x: A  B adding a
copy of the formula in the multiset CondContr:
If x: A  B  K
K  { x: A  B } | CondContr  { x: A  B } | , y: B
K  { x: A  B } | CondContr  { x: A  B } | 
(L)1
K | CondContr | , x: A  B

, x

A
y
How to obtain a decision procedure
• The (L) rule is “split” in three rules, to keep into account of the
necessary application of (ContrL).
1. The second rule is applied if x: A  B has already been contracted
in that branch (i.e. belongs to K); it decomposes the principal formula
x: A  B without adding any copy of it:
If x: A  B  K
K | CondContr | , y: B
K | CondContr | 
(L)2
, x
K | CondContr | , x: A  B

A
y

How to obtain a decision procedure
• The (L) rule is “split” in three rules, to keep into account of the
necessary application of (ContrL).
2. The third rule decomposes a contracted formula x: A  B in
CondContr, without adding a copy of it:
K  { x: A  B } | CondContr | 
 x
K  { x: A  B } | CondContr | , y: B
(L)3
A
y

K  { x: A  B } | CondContr  { x: A  B } | 

How to obtain a decision procedure
• We have improved SeqS calculi presented in [OlivettiPozzato03],
where the rule (L) was split in two rules;
• Reduced number of application of (implicit) contraction in each
branch: better performances
• Improved version of the graphical user interface
• Many features inherited from CondLean
4
Design of
CondLean 2.0
Design of CondLean 2.0
• CondLean 2.0 is a Prolog implementation of BSeqS calculi; it is
written in SICStus Prolog and it is inspired by leanTAP, introduced by
Beckert and Posegga 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 2.0
• CondLean 2.0 is a Prolog implementation of BSeqS calculi; it is
written in SICStus Prolog and it is inspired by leanTAP, introduced by
Beckert and Posegga 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.
• The sequent calculi are implemented by the predicate
prove(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 , and Labels is the list of labels introduced in that branch .
Design of CondLean 2.0
• Each clause of predicate prove implements one axiom or rule of
BSeqS.
• The clauses of prove are ordered to postpone the application of the
branching rules.
Design of CondLean 2.0
• Each clause of predicate prove implements one axiom or rule of
BSeqS.
• 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 2.0
Example 2: clause implementing (R):
(R)
, x

A
y
, y: B
, x: A  B
prove([LitSigma,TransSigma,ComplexSigma],
[LitDelta,TransDelta,ComplexDelta],Labels):
select([X,A => B],
ComplexDelta,ResComplexDelta),!,
createLabels(Y,Labels),
put([Y,B], LitDelta, ResComplexDelta,
NewLitDelta, NewComplexDelta),
prove([LitSigma, [[X,A,Y]|TransSigma],
ComplexSigma],[NewLitDelta,TransDelta,
NewComplexDelta],[Y|Labels]).
Design of CondLean 2.0
• For systems BSeqMP and BSeqID+MP the predicate prove has two
additional arguments:
prove(K, CondContr, Sigma, Delta, Labels)
• K and CondContr are the auxiliary sets of BSeqS calculi, used to
control the application of (L)
Design of CondLean 2.0
Example 3: clause implementing (L)1:
K  { x: A  B } | CondContr  { x: A  B } | , y: B

A
y
K  { x: A  B } | CondContr  { x: A  B } | 
, x
(L)1
K | CondContr | , x: A  B 
prove(K,CondContr,[LS,TS,CS],[LD,TD,CD],Labels):select([X,A => B],CS,ResCS),
\+member([X,A => B],K),
select(Y,Labels),
put([Y,B],LS,ResCS,NewLS,NewCS),
prove([[X,A => B]|K],[[X,A => B]|CondContr],
[NewLS,TS,NewCS],[LD,TD,CD],Labels),
prove([[X,A => B]|K],[[X,A => B]|CondContr],
[LS,TS,ResCS],[LD,[[X,A,Y]|TD],CD],Labels).
Design of CondLean 2.0
• We present three different implmentations for our theorem provers:
1. Constant labels version;
2. Free-variables version;
3. Heuristic version.
Design of CondLean 2.0
1. Constant labels version
• This version makes use of Prolog constants to represent SeqS’s
labels, introdouced by the (R) rule.
Design of CondLean 2.0
1. Constant labels version
• This version makes use of Prolog constants to represent SeqS’s
labels, introdouced by the (R) rule.
• 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 2.0
2. Free-variables version
• In this implementation, CondLean 2.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 2.0
Free variable
(L)

, x
A
, V: B
V
, x: A  B


Each free variable will be then istantiated by Prolog’s pattern matching
to apply either the (EQ) rule, or to close a branch with an axiom.
Design of CondLean 2.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 2.0
3. Heuristic version
• This implementation performs a “two-phase” computation:
Design of CondLean 2.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;
Design of CondLean 2.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.
Design of CondLean 2.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 2.0
• The performances of the three versions are promising.
• We have tested CondLean 2.0 - free variable version 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 2.0
at the following address:
www.di.unito.it/~olivetti/CondLean 2.0
5
Future work
Future work
• We are working on some extensions of CondLean 2.0 to stronger
conditional systems
• We have found cut-free and terminating calculi for conditional logics
CS and CEM (Stalnaker logic):
System
CK+CS
CK+CEM
Axiom
(A  B)  (A  B)
Selection function property
w  [ A ]  f (w, [ A ])  {w}
(A  B)  (A  B)
| f (x, [ A ]) |  1
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.
[OlivettiPozzatoSchwind04] Nicola Olivetti, Gian Luca Pozzato and
Camilla B. Schwind. A Sequent Calculus and a Theorem Prover for
Standard Conditional Logics. Technical Report 81/04, Dipartimento di
Informatica, Università degli Studi di Torino, Italy, November 2004.
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.