Logic for Computer Scientists/Predicate Logic/SATCHMO

< Logic for Computer Scientists‎ | Predicate Logic

Contents

SATCHMOEdit

The SATCHMO Theorem Prover was one of the first systems which used model generation, i.e. a bottom-up proof procedure. The prover was given by a small Prolog-program, which implements a tableau proof procedure. One restriction is that it requires range restricted formulae.

Definition 30Edit

A first order clause is called range restricted if every variable which occurs in the head occurs in the body as well.

  1. Convert clauses to range restricted form:
  2. assert range-restricted clauses and dom clauses in Prolog database.
  3. Call satisfiable:
kill satisfiable :-    assume(X) :- asserta(X).     
       (Head <- Body)            assume(X) :-  
       Body, not Head, !,          retract(X), !, fail.  
       component(HLit, Head),      component(E, (E ; _)).      
       assume(HLit),               component(E, (_ ; R)) :-    
       not false,                   !, component(E, R).   
       satisfiable.                component(E, E).  
  satisfiable.

First-Order completeness via Level-Saturation modification. This proof procedure implements Hyper Tableaux in the ground case.

Hyper Tableau - Ground CaseEdit

Hypertableau.png

All open branches consist of positive literals only Take the following clause set as an example Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle \{ \to A, \quad \to B, \quad A\land B \to C\lor D,\quad A\land B \to E\lor D,\quad A\land C \to \}}

Hypertableau1.png

Definition 31 (Literal tree, Clausal Tableau)Edit

A literal tree is a pair consisting of a finite, ordered tree and a labeling function that assigns a literal to every non-root node of .

The successor sequence of a node in an ordered tree is the sequence of nodes with immediate predecessor , in the order given by .

A (clausal) tableau of a set of clauses is a literal tree in which, for every successor sequence in labeled with literals , respectively, there is a substitution and a clause with for every . is called a tableau clause and the elements of a tableau clause are called tableau literals.

Definition 32 (Branch, Open and Closed Tableau, Selection Function)Edit

A branch of a tableau Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): T is a sequence () of nodes in such that is the root of , Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle N_i} is the immediate predecessor of for Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle 0 \leq i < n} , and is a leaf of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): T . We say branch Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle b= N_0,\ldots , N_n} is a prefix of branch , written as or , iff for some nodes Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle N_{n+1},\ldots , N_{n+k}} , . The branch literals of branch are the set . We find it convenient to use a branch in place where a literal set is required, and mean its branch literals. For instance, we will write expressions like Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle A \in b} instead of Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle A \in lit(b) } .

In order to memorize the fact that a branch contains a contradiction, we allow to label a branch as either open or em closed. A tableau is closed if each of its branches is closed, otherwise it is open.

A selection function is a total function which maps an open tableau to one of its open branches. If we also say that is selected in by .

Note that branches are always finite, as tableaux are finite. Fortunately, there is no restriction on which selection function to use. For instance, one can use a selection function which always selects the "leftmost" branch.

Definition 33 (Hyper Tableau - Ground Case)Edit

Let be a finite set of clauses and be a selection function. Hyper tableaux for are inductively defined as follows:
Initialization step: A one node literal tree is a hyper tableau for . Its single branch is marked as "open".

Hyper extension step: If

  1. is an open hyper tableau for , (i.e. is selected in by ) with open leaf node , and
  2. Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle C = A_1, \ldots , A_m \gets B_1, \ldots , B_n} is a clause from (, ), called extending clause in this context, and
  3. such that (referred to as hyper condition)

then the literal tree is a hyper tableau for , where is obtained from by attaching child nodes to with respective labels



and marking every new branch Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle (b,M_1),\ldots ,(b,M_m)} with positive leaf as "open", and marking every new branch with negative leaf as "closed".

Minimal Model ReasoningEdit

The clause set obviously has two different models: Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle \{ A,\;B \}} and Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle \{ B \}} . Under set inclusion these models can be compared and there are some tasks where it is appropriate to compute the (or in general a) smallest one. This is for example the case with

  • Knowledge Representation, Circumscription
  • Basis for default negation (GCWA)
  • Applications: Deductive database updates, Diagnosis

There are basically two different methods to compute minimal models.

Minimal Model Reasoning – Niemel¨a’s ApproachEdit

Given a set of ground clauses the methods applies a model generating procedure, e.g. hyper tableau, which is able to generate all models.

Lemma 1: For every minimal model for there is a branch with literals .

Assume that Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle \Sigma} is the set of atoms, which occur in the head of a clause from , than the following Lemma holds.

Lemma 2: is a minimal model for iff

This offers a general method: Generate model candidates, and test with Lemma 2.

is not a minimal model in our example from above, because iff is unsatisfiable, which is not the case, hence does not correspond to a minimal model and hence the branch is closed.

is minimal because Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle M \cup \{ \gets A \} \models \{B\} } iff is unsatisfiable. This is the case and hence is minimal and the branch remains open.

Properties: Soundness (by Lemma 2) Completeness (by Lemma 1), space efficiency.

Minimal Model Reasoning – Bry& Yayha‘s ApproachEdit

As an example we have the set Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "/mathoid/local/v1/":): {\displaystyle M = \{ A \lor B \lor C \gets, \quad B \gets A, \quad D \gets B\}}

Minimalmodelreasoning.png


Lemma: With complement splitting, the leftmost open branch is a minimal model for .

General method: Repeat: generate minimal model , add to . Properties: Soundness (by Lemma) Completeness as before, possibly exponentially many new clauses .