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

- Convert clauses to range restricted form:
- assert range-restricted clauses and dom clauses in Prolog database.
- 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

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 \}}**

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

- is an open hyper tableau for , (i.e. is selected in by ) with open leaf node , 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 C = A_1, \ldots , A_m \gets B_1, \ldots , B_n}**is a clause from (, ), called*extending clause*in this context, and- 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\}}**

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