Dipartimento di Informatica - Università degli studi di Torino

Dipartimento di Informatica - Università degli studi di Torino

CondLean 2.0: a Theorem Prover for

standard Conditional Logics

Nicola Olivetti – Gian Luca Pozzato

• 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

Outline

11

CConditional logicsonditional 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

• 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

Syntax

Conditional logics

Semantics

• We consider the selection function semantics; the model is a triple:

< W, f, [ ] >

Conditional logics


Semantics

- W is a non-empty set of items called worlds;

Conditional logics

< W, f, [ ] >

Semantics


- f is a function f: W x 2W 2W , called the selection function;

Conditional logics


< W, f, [ ] >

Semantics


- [ ] is an evaluation function [ ] : ATM 2W.

Conditional logics

- f is a function f: W x 2W 2W , called the selection function;


< W, f, [ ] >

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

Semantics

• 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:

RCEA:

RCK:

A A B

B

A B

(A C) (B C)

(A1 A2 … An) B

(C A1 C A2 … C An) (C B)

Conditional logics - System CK

With some properties of the selection function, we have the following extensions:

System Axiom Selection function property

Conditional logics

Systems CK{+MP}{+ID}

CK+ID A A f (x, [ A ]) [ A ]



Conditional logics


CK+MP (A B) (A B) w [ A ] w f (w, [ A ])CK+ID A A f (x, [ A ]) [ A ]



Conditional logics


CK+MP+ID(A B) (A B) w [ A ] w f (w, [ A ])

A A f (x, [ A ]) [ A ]

CK+MP (A B) (A B) w [ A ] w f (w, [ A ])CK+ID A A f (x, [ A ]) [ A ]



Conditional logics


22

SSequent Calculi SeqSequent 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:


Labelled formulas, like x: A;




x yA transition formulas, like .





• A labelled formula x: A represents that the formula A is true in the world x.






• A transition formula represents that y f ( x, [ A ] ).x yA

• A labelled formula x: A represents that the formula A is true in the world x.







Theorem (soundness and completeness of SeqS): is valid iff it is derivable in SeqS.

33

HHow to obtain a ow to obtain a decision proceduredecision procedure

• SeqS calculi have the following contraction rules:

, F

, F, F(ContrR), F

, F, F (ContrL)

How to obtain a decision procedure

, F

, F, F(ContrR), F

, F, F (ContrL)

• 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.

• SeqS calculi have the following contraction rules:


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).


• 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.


1. SeqID is complete without the contraction rules.


• This analysis is inspired by the work made by Luca Viganò for modal logic T [Viganò00]

• 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.



2.1. SeqMP and SeqID+MP are complete without the (ContrR) rule.

• Here are the BSeqS calculi presented in [OlivettiPozzatoSchwind04]:

• 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:

K | CondContr | , x: A B

K { x: A B } | CondContr { x: A B } | ,

(L)1

x yA



K { x: A B } | CondContr { x: A B } | , y: B

If x: A B K

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 | ,

(L)2

x yA

K | CondContr | , y: B

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: A B } | (L)3

x yA

K { x: A B } | CondContr | , y: B

K { x: A B } | CondContr |

• 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


44

DDesign of esign of

CondLean 2.0CondLean 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

• 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 .


• 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.


• 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:

prove([_,_,ComplexSigma],[_,_,ComplexDelta],_):- member(F,ComplexSigma), member(F,ComplexDelta),!.

, F , F(AX)


• 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 2: clause implementing (R):

prove([LitSigma,TransSigma,ComplexSigma],

, x: A B

, , y: B(R) x yA


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]).

[LitDelta,TransDelta,ComplexDelta],Labels):


• 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)

Example 3: clause implementing (L)1:

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).


K { x: A B } | CondContr { x: A B } | ,(L)1

x yA

K { x: A B } | CondContr { x: A B } | , y: B

prove(K,CondContr,[LS,TS,CS],[LD,TD,CD],Labels):-


• We present three different implmentations for our theorem provers:

1. Constant labels version;

2. Free-variables version;

3. Heuristic version.


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:

, x: A B

,(L)

x yA , y: B


1. Constant labels version

• This version makes use of Prolog constants to represent SeqS’s labels, introdouced by the (R) rule.

• If there are n labels to choose, the computation might succeed only after n-1 backtracking steps, with a significant loss of efficiency.

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].


, x: A B

,(L)

x VA , V: 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.

Free variable


• 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.


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.





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.


• 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 6 9 11 15

5 500 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

55

FFuture workuture 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):

Future work

CK+CEM (A B) (A B)

CK+CS

| f (x, [ A ]) | 1


w [ A ] f (w, [ A ]) {w}(A B) (A B)

66

RReferenceseferences

References

[BeckertPosegga96] Bernard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 15(3), pp. 339-358.

[BeckertGorè97] Bernard Beckert and Rajeev Gorè. Free Variable Tableaux for Propositional Modal Logics. Tableaux-97, LNCS 1227, Springer, pp. 91-106.

[Gabbay96] Dov. M. Gabbay. Labelled deductive systems (vol. i). Oxford logic guides, Oxford University Press.

References

[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.

[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.

References

[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.

[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 athttp://www.di.unito.it/~pozzato/tesiPozzato.html

Dipartimento di Informatica - Università degli studi di Torino

Documents

Transcript of Dipartimento di Informatica - Università degli studi di Torino