Week 03: Propositions and Inference

Simple Language: Propositional Definite Clauses

Atom: symbol starting with lower case letter
Body: atom or of the form $b_1 \land b_2$ , where $b_1$ and $b_2$ are bodies
Definite clause: atom or rule of form $h \leftarrow b$ , where $h$ is an atom and $b$ is a body. If it has an empty body, is called an atomic clause/fact
Knowledge base: set of definite clauses

Interpretation

An interpretation assigns a truth value to each atom. Thus, there are $2^{num\_atoms}$ possible interpretations.

Body $b_1 \land b_2$ is true in $I$ if both $b_1$ and $b_2$ are true in $I$
Rule $h \leftarrow b$ is false in $I$ if $b$ is true and $h$ is false
- i.e. If $b$ is true, $h$ must be true
Knowledge base $KB$ is true in iff every clause in $KB$ is true in $I$

Models and Logical Consequences

Model of a set of clauses: interpretation in which all the clauses are true
If is $KB$ a set of clauses and is $g$ a conjunction of atoms, $g$ is a logical consequence of $KB$ ( $KB \models g$ ) if is true in every model of $KB$

Example: $$ KB = \begin{cases} p \leftarrow q,\ q,\ r \leftarrow s \end{cases} $$ $m = (p = true, q = true, r = false, s = false)$ would be a model of $KB$ .

Proof Procedures

A possibly non-deterministic algorithm for deriving consequences of a knowledge base
Given a proof procedure, $KB \vdash g$ means $g$ can be derived from the knowledge base $KB$
A proof procedure is sound if $KB \vdash g$ implies $KB \models g$
- Every consequence it finds is true
A proof procedure is complete if $KB \models g$ implies $KB \vdash g$
- All consequences are found by the procedure

Bottom-Up Proof Procedure

If $h \leftarrow b_1 \land \cdots \land b_m$ is a clause in the knowledge base and each $b_i$ has been derived (all are consequences), then can be derived. This method is called forward chaining.

First, set $c:=\{\}$ . Then, select a clause $h \leftarrow \; b_1 \land \cdots \land b_m$ in $KB$ such that:

$b_i \in C \;\forall i$
$h \notin C$

Then set $C := C \cup \{h\}$ .

Repeat until no more clauses can be selected. (Only atomic clauses can be added to the set at the beginning).

$KB \vdash g$ if $g \in C$ at the end of the procedure.

Proof of soundness

If there is a $g$ such that $KB \vdash g$ but $KB \nvDash g$ , there must be some atoms added to $C$ which aren’t true in every model of $KB$ . Call the first such atom $h$ .

Thus, there must be clause of the form $h \leftarrow b_2 \land \dots \land b_m$ . As $h$ is the first wrong atom, each $b_i$ must be true in some interpretation $I$ . Thus, this clause must be false in $I$ ; thus, cannot be a model of $KB$ .

Fixed Point

The $C$ generated at the end of the bottom-up algorithm is called a fixed point.

If $I$ is the interpretation in which every element of the fixed point is true, and every other atom is false:

$I$ is a model of $KB$
- If $h \leftarrow b_1 \land \dots \land b_m$ in $KB$ is false in $I$ . Then, $h$ is false but each $b_i$ is true in $I$
  - Thus, $h$ can be added to $C$ (WHY?), meaning it is not the fixed point
$I$ is called a minimal model

Proof of Completeness

Suppose $KB \models g$ ; $g$ is true in all models of $KB$
Thus, $g$ is true in the minimal model
Thus, $g$ is in the fixed point
Thus, $g$ must have been generated by the bottom up algorithm
Thus, $KB \vdash g$

Top-Down Procedure

Search backwards from a query to determine if it is a logical consequence of $KB$ (i.e. asking if an atom is true).

An answer clause: $yes \leftarrow a_1 \land \dots \land a_m$ .

The SLD resolution of the answer clause on atom $a_i$ with the clause $a_i \leftarrow b_1 \land \dots \land b_p$ is another answer clause:

yes \leftarrow \; a_1 \land \dots \land a_{i-1} \land b_1 \land \dots \land b_p \land a_{i+1} \land \dots \land a_m

Basically: replace the atom with its clause, repeating until no more replacements can be made.

An answer is an answer clause $m=0$ with $m=0$ ; that is, the answer clause is $yes \leftarrow$ .

Derivations

Derivation of query $? q_1 \land \dots \land q_k$ is a sequence of answer clauses $\gamma_0, \dots, \gamma_n$ such that:

$\gamma_0$ is the answer clause $yes \leftarrow q_1 \land \dots \land q_k$
$\gamma_i$ is the answer clause obtained by resolving $\gamma_{i-1}$
$\gamma_n$ is an answer

Procedure

To solve the query $? q_1 \land \dots \land q_k$ :

$ac := yes \leftarrow q_1 \land \dots \land q_k$
Until $ac$ is an answer:
- Select $a_i$ atom from the body of $ac$
  - Choose a clause $C$ from $KB$ with $a_i$ as the head ( $a_i \leftarrow body$ )
  - Replace $a_i$ with the body of $C$
- If the clause is just a definition (e.g. $e.$ ), then it does not get replaced with anything; $ac$ shrinks

Either don’t-care non-determinism, in which case if a selection does not lead to a solution, there is no point in trying other alternatives, or don’t-know-non-determinism, in which other choices may lead to a solution.

A successful derivation would return $ac := yes$ .

A failing derivation would return something in the form $ac := yes \leftarrow a_0 \land \dots \land a_n$ . This does not mean it cannot be derived, just that it failed. Use DFS; backtrack.