Predicate Calculus

It is a mathematical language used to encode pieces of domain knowledge and reason with them to derive new pieces of knowledge or draw inferences.

A predicate is an expression of one or more variables defined on some specific domain of discourse.

A predicate with variables can be made a proposition by either assignming a value to the variables or by quantifying the variables.

Example:

\[\underbrace{\text{Ram }}_{\text{Subject}} \underbrace{\text{is a student}}_{\text{Predicate}}\]

may be represented as \(P(x)\), where:

  • \(P\) is the predicate "is a student"

  • \(x\) may take the value "Ram" (or any other student)

@TODO: insert predicate calculus diagram

What is Knowledge?

Knowledge may be:

  • Facts, e.g.

    • "The earth moves round the sun"

    • "Bibhutibhusan is the author of Pather Panchali"

  • Concepts, e.g.

    • "In physics, weight of an object is the force of gravity on the object"

    • "Animals that live in water are called aquatic animals"

    • "A cricketer is one who can play cricket"

  • Rules, e.g.

    • "Everyone who has passed H.S. is eligible to study B.E."

    • "Eligibility for studying computer science is knowledge of mathematics"

  • Heuristics, e.g.

    • "The questions which were set for the exam in the last year are not set for exam in the current year."

Elements of Predicate Calculus

The elements of predicate calculus are:

  • Syntax of predicate calculus sentences/well formed formulas (WFFs):

    • Atomic Formulas

    • Alphabets

    • Literals

    • WFFs

  • Rules for drawing inferences

Atomic Formulas

These are the smallest sentences of predicate calculus.

Atomic Formula \(=\) Predicate Symbol \(+\) Terms

where:

  • Predicate Symbol represents the relation in a domain of discourse

  • Terms may be:

    • constants

    • variables

    • functions

Examples:

  • "Homer is the author of Iliad"

    • Author-of(Iliad, Homer)

      • Author-of \(\rightarrow\) Predicate Symbol

      • {Iliad, Homer} \(\rightarrow\) Terms (constants)

    • "Father of John and mother of John are spouse"

      • Spouse(father-of(John), mother-of(John))

    • "Husband of a wife and wife of the same husband are spouse"

      • \( (\forall x) \) Spouse(husband(\(x\)), wife(husband(\(x\))))

Alphabets

The alphabet of the language of predicate calculus:

Set of capital letters \(\cup\) Set of small letters \(\cup\) Set of connectives \(\cup\) Set of parentheses \(\cup\) {\(-\), \(,\)}

Literals

Literals may be atomic formulas or their negations

E.g. "Aristotle is not the author of Iliad"

  • ~Author-of(Iliad, Aristotle)

Well Formed Formulas (WFFs)

One or more atomic formulas, combined with connectives.

Connectives are boolean operators

Symbol Meaning

\(\land\)

and

\(\lor\)

or

\(\sim\)

not

\(\Rightarrow\)

implication

"All positive integers are natural numbers"

  • \( (\forall x) \) [Positive-Integer(\(x\)) \(\Rightarrow\) Natural-No(\(x\))]

"Every book has some author"

  • \( (\forall x) \) [Book(\(x\)) \(\Rightarrow\) \( (\exists y) \) Author-of(\(x, y\))]

Interpretation of Well-Formed Formulas

Interpretation entails:

  • Truth value of a WFF

  • Interpretation for constituent atomic formulas

Interpretation of an atomic formula is carried out by:

  • assigning correspondence between the elements of the language (i.e. constants, variables, functions and predicates)

  • entities of the world/domain of discourse (e.g. objects, relations and functions)

An atomic formula \(\rightarrow\) Interpretation \(\rightarrow\) A statement of the domain

Once an interpretation for an atomic formula has been defined, the formula has been defined, the formula has a true value just when the corresponding statement about the domain is true.

Otherwise, it has false value.

Interpretation of WFFs define the semantics of predicate calculus language.

Example: Consider the following WFFs

  • Clear(B)

  • On(B, A)

  • On(C, F) \(\land\) On(A, C) \(\land\) On(B, A)

block world 01
Elements of Predicate Calculus Entities of the World/Domain of Discourse

A

\(\textbf{A}\)

B

\(\textbf{B}\)

C

\(\textbf{C}\)

F

\(\textbf{F}\)

On

On \( = \{\langle \textbf{B}, \textbf{A} \rangle, \langle \textbf{A}, \textbf{C} \rangle, \langle \textbf{C}, \textbf{F} \rangle\}\)

Clear

Clear \( = \{ \langle \textbf{B} \rangle \}\)
Well Formed Formulas Statement of the world/domain Truth Value

On(A, B)

\(\langle A, B \rangle \notin \) On

F

Clear(B)

\(\langle A \rangle \in \) Clear

T

On(C, F)

\(\langle C, F \rangle \in \) On

T

On(A, B) \(\land\) ~On(A, B)

T

@TODO insert diagram of mapping pred calc -> real world elements

Models

An interpretation is said to be satisfying a WFF if the WFF has a True value under the representation.

An interpretation that satisfies a WFF is a model of that WFF.

Two WFFs are equivalent if and only if their truth values are identical under all interpretations (that is, if and only if the two WFFs logically entail each under).

A WFF that has a true value under all interpretations is called a valid WFF.

Ground WFFs are WFFs that are made of strictly constant terms.

Valid ground WFFs are called tautologies, e.g. \(P(A) \Rightarrow [P(A) \lor P(B)]\)

Any WFF that does not have a model is inconsistent or unsatisfiable, e.g. \(P \land \sim P\).

Logical Entailment

A WFF \(w\) has a true value under all those interpretations for which each WFF in a set \(\Delta\) has a true value, then:

\[\Delta \models w\]

For example:

  • \( (\forall x) P(x) \models P(A) \)

  • \( \{ ( \forall x) [\sim P(x) \lor Q(x)], (\forall x) P(x) \} \models (\forall x) P(x) \)

  • \( \{ ( \forall x) (\forall y) [P(x) \lor Q(y)], (\forall z) [R(x) \lor Q(A)] \} \)

    \( \hspace{1em} \models (\forall x) (\forall y) [P(x) \lor Q(y)] \)

Semantics of Quantifiers

Universal Quantifiers

\[(\forall v) W(v)\]

Example: Block world problem

Let \(w = (\forall) x [\text{On}(x, c) \Rightarrow \sim \text{Clear}(C)]\)

block world 02

  1. \(x = A\)

    \(\langle A, C \rangle \notin \text{On}\)

    \(\langle C \rangle \in \text{Clear}\)

    The assignment \(x = A\) results in a True value for \(w\).

  2. \(x = B\)

    \(\langle B, C \rangle \notin \text{On}\)

    \(\langle C \rangle \in \text{Clear}\)

    2nd assignment \(x = B\) results in a True value for \(w\).

  3. \(x = C\)

    \(\langle C, C \rangle \notin \text{On}\)

    \(\langle C \rangle \in \text{Clear}\)

    3rd assignment \(x = C\) results in a True value for \(w\).

  4. \(x = F\)

    \(\langle F, C \rangle \notin \text{On}\)

    \(\langle C \rangle \in \text{Clear}\)

    4th assignment \(x = F\) results in a True value for \(w\).

Existential Quantifiers

\[(\exists u) W(u)\]

This has a True value (under a given assignment to objects, functions and relations) just in case \(w(u)\) has a True value for at least one assignment of the variable symbol \(u\) to objects in the domain

Useful Equivalences

  • \(\sim(\forall x) w(x) \equiv (\exists x) (\sim w(x))\)

  • \(\sim(\exists x) w(x) \equiv (\forall x) (\sim w(x))\) \(\)

  • \((\forall x) w(x) \equiv (\forall y) w(y)\)

  • \((\exists x) w(x) \equiv (\exists y) w(y)\)

  • \( (\forall x) [w_1(x) \land w_2(x)] \equiv (\forall x_1)w_1(x_1) \land (\forall x_2) w_2(x_2) \)

  • \( (\exists x) [w_1(x) \lor w_2(x)] \equiv (\exists x_1)w_1(x_1) \lor (\exists x_2) w_2(x_2) \)

Rules of Inferences

They are required to derive new sentences/formulas from the existing ones

Modus Ponens

\[\begin{align} &w_1\\ &w_1 \rightarrow w_2 \\ &\rule{6em}{0.05em} \\ &w_2 \text{ (inference)} \end{align}\]

Here, \(\Delta = \{w_1, w_1 \Rightarrow w_2\} = \{w_1, \sim w_1 \lor w_2\}\)

Therefore,

\[\Delta \models w_2\]

Universal Specialization

\[\begin{aligned} &(\forall x) w(x) \hspace{3em}\\ &\rule{4em}{0.05em} \\ &w(A) \end{aligned} \begin{aligned} \underbrace{\{A/x\}}_{\text{Substitution }=\;\{\text{term}/\text{value}\}} \end{aligned}\]

Combination

\[\begin{aligned} &w_1(A)\\ &(\forall x) w_1(x) \Rightarrow w_2(x) \hspace{3em}\\ &\rule{9em}{0.05em} \\ &w_2(A) \text{ (inference)} \end{aligned} \begin{aligned} \underbrace{\{A/x\}}_{\text{Substitution }} \end{aligned}\]

Example

  1. Three is a positive integer

  2. All positive integers are natural numbers

  3. Is three a natural number?

Further,

  1. All natural numbers are used for counting.

  2. Is three used for counting?

  1. \( \text{+veInteger(THREE)} \)

  2. \( (\forall x) \text{+veInteger}(x) \Rightarrow \text{Natural-No}(x) \hspace{2em} \{\text{THREE}/x\} \)

  3. \( \text{Natural-No}(x) \)

  4. \( (\forall y) \text{Natural-No}(y) \Rightarrow \text{Used-for-Counting}(y) \hspace{2em} \{\text{THREE}/y\} \)

  5. \( \text{Used-for-Counting}(x) \)

Substitutions

A substitution \(s\) is in general represented with a set of ordered pairs as follows:

\[s = \{t_1/v_1, t_2/v_2, t_3/v_3\}\]

\(t_i/v_i\) represents substitution of a variable by its term \(t_i\) and \(v_i\) must not occur in it.

Example: Substitutions Applied on WFFs

Notation: \(\text{WFF}_\circ \text{substitution}\) or \(w_\circ s\)

\[\begin{align} s_1 &= {A/x, w/y}\\ s_2 &= {c/x, A/y}\\ s_3 &= {g(z)/x, A/y}\\ s_4 &= {A/y} \end{align}\]
\[\begin{align} \text{Let } w &= P(x, f(y), B)\\ w_\circ s_1 &= P(z, f(w), B)\\ w_\circ s_2 &= P(c, f(A), B)\\ w_\circ s_3 &= P(g(z), f(A), B)\\ w_\circ s_4 &= P(x, f(A), B) \end{align}\]

Composition of Substitutions

Notation: \(s_{1\circ}s_2\)

Rules

  1. Apply \(s_2\) to the terms of \(s_1\) to produce \(s_1'\)

  2. Form a set by adding any pair from \(s_2\) having variables not occurring among the variables of \(s_1\)

Example:

\[\begin{align} s_1 &= \{g(x, y)/z\}\\ s_2 &= \{A/x, B/y, C/w, D/z\} = s_{2\circ}s_1\\ s_{1\circ}s_2 &= \{g(A, B)/z, A/x, B/y, C/w\}\\ \end{align}\]
Note
 composition of substitutions is not in general commutative, but it is associative

Unification

Let \(\{w_i | i = 1, 2, \dots\}\) be a set of expressions of WFFs.

\(\{w_i | i = 1, 2, \dots\}\) is called unifiable if there exists a substitution \(s\) such that

\[w_{1\circ}s = w_{2\circ}s = w_{3\circ}s = \cdots\]

Example:

\[\begin{align} \{w_i | i = 1, 2, \dots\} &= \{P(x, f(y), B), P(x, f(B), B)\}\\ s &= \{A/x, B/y\}\\ \{w_i | i = 1, 2, \dots\}_\circ s &= \{P(A, f(B), B)\}\\ \end{align}\]

  • \(s\) is called a unifier \(\{w_i | i = 1, 2, \dots\}\)

Unifier of \(\{w_i | i = 1, 2, \dots\}\) may not be unique, e.g. \(\{B/y\}\) is yet another unifier of \(\{P(x, f(y), B)\}\).

Most General Unifiers (MGUs)

An \(\text{mgu}\) of a set of predicate calculus WFFs \(\{w_i | i = 1, 2, \dots\}\) has the property that:

  • if \(s\) is any unifier of \(\{w_i | i = 1, 2, \dots\}\), giving \(\{w_i | i = 1, 2, \dots\}_\circ s\) then there exists a substitution \(s'\) such that

\[\{w_i | i = 1, 2, \dots\}_\circ s = \{w_i | i = 1, 2, \dots\}_\circ \text{mgu}_\circ s'\]

Example: \(\{w_i | i = 1, 2, \dots\} = \{F(x), F(g(y))\)

\[\begin{align} &\text{Let } s_1 = \{g(A)/x, A/y\}\\ &\text{mgu} = \{g(y)/x\}\\ &\{F(x), F(g(y))\}_\circ s_1\\ &\hspace{0.5em} = \{F(g(A), F(g(A))\}\\ &\hspace{0.5em} = \{F(g(A))\}\\ &\hspace{0.5em} = \{F(x), F(g(y))\}_\circ\underbrace{\{g(y)/x\}}_\text{mgu}\circ\underbrace{\{A/y\}}_{s_1'}\\ \end{align}\]
\[\begin{align} &\text{Let } s_2 = \{g(B)/x, B/y\}\\ &\hphantom{\text{Let }} s_2' = \{B/y\}\\ &s_{2\circ}s_2' = \{g(y)/x\}_\circ \{B/y\}\\ \end{align}\]

\(\star\) So an \(\text{mgu}\) must be common in all unifiers of \(\{w_i | i = 1, 2, \dots\}\)

Example: \(\{w_i | i = 1, 2, \dots\} = \{P(x, f(y), B), P(x, f(B), B)\}\)

\[\begin{align} &s = \{A/x, B/y\}\\ &\text{mgu} = \{B/y\}\\ &s = \{B/y\}_\circ \{A/x\}\\ \end{align}\]

Disagreement Set

The disagreement set \(D\) of a set of expressions \(\{w_i | i = 1, 2, 3, \dots\}\) is obtained as follows.

Steps:

  1. Compare each symbol of all expressions in \(\{w_i | i = 1, 2, \dots\}\) from left to right

  2. Extract the complete sub-expression whose first symbols do not agree in step 1

  3. Form the disagreement set, a collection of all the above mentioned sub-expressions

  4. Stop

Example

Let \(\{w_i | i = 1, 2, \dots\} = \{P(f(x), \)\(\underset{\uparrow}{g(y)}\)\(, A), P(f(x), \)\(\underset{\uparrow}{B}\)\(, h(u))\}\)

\(D = \{g(y), B, A, h(u)\}\)

Algorithm for Finding mgu

Steps:

  1. \(k = 0\)

  2. \(\text{mgu}_k = \{\}\)

  3. while (\( \{w_i | i = 1, 2, \dots\}_\circ\text{mgu}_k \neq\) singleton set) {

  4. \(D_k =\) disagreement set of \(\{w_i | i = 1, 2, \dots\}_\circ\text{mgu}_k\)

  5. If there is a substitution \(\{t/u\}\) which can be formed with \({D_k}\), then \(\Delta\text{mgu} = \{t/u\}\)

  6. else stop

  7. \( \text{mgu}_{k+1} = \text{mgu}_{k\circ}\Delta\text{mgu}\)

  8. \(k = k + 1\)

  9. }

  10. Print \(\text{mgu}_k\)

  11. Stop

Example

Let \(\{w_i | i = 1, 2, \dots\} = \{P(x, z, y), P(w, u, w), P(A, u, u)\}\)

Initially

  • \(k = 0\)

  • \(\text{mgu} = \{\}\)

Pass #1

  • \(\{w_i | i = 1, 2, \dots\}_\circ \text{mgu}_0 = \{P(x, z, y), P(w, u, w), P(A, u, u)\}\)

  • \(D_0 = \{x, w, A, z, u, y\}\)

  • \(\Delta \text{mgu} = \{A/x\}\)

  • \(\text{mgu}_1 = \text{mgu}_{0\circ} \Delta \text{mgu} = \{A/x\}\)

  • \(k = 0 + 1 = 1\)

Pass #2

  • \(\{P(x, z, y), P(w, u, w), P(A, u, u)\}_\circ \text{mgu}_1 = \{P(A, z, y), P(w, u, w), P(A, u, u)\}\)

  • \(D_1 = \{w, A, z, u, y\}\)

  • \(\Delta \text{mgu} = \{A/w\}\)

  • \(\text{mgu}_2 = \text{mgu}_{1\circ} \Delta \text{mgu} = \{A/x, A/w\}\)

  • \(k = 1 + 1 = 2\)

Pass #3

  • \(\{P(x, z, y), P(w, u, w), P(A, u, u)\}_\circ \text{mgu}_2 = \{P(A, z, y), P(A, u, A), P(A, u, u)\}\)

  • \(D_2 = \{A, z, u, y\}\)

  • \(\Delta \text{mgu} = \{A/z\}\)

  • \(\text{mgu}_3 = \text{mgu}_{2\circ} \Delta \text{mgu} = \{A/x, A/w, A/z\}\)

  • \(k = 2 + 1 = 3\)

Pass #3

  • \(\{P(x, z, y), P(w, u, w), P(A, u, u)\}_\circ \text{mgu}_3 = \{P(A, A, y), P(A, u, A), P(A, u, u)\}\)

  • \(D_3 = \{A, u, y\}\)

  • \(\Delta \text{mgu} = \{A/y\}\)

  • \(\text{mgu}_4 = \text{mgu}_{3\circ} \Delta \text{mgu} = \{A/x, A/w, A/z, A/y\}\)

  • \(k = 3 + 1 = 4\)

Pass #4

  • \(\{P(x, z, y), P(w, u, w), P(A, u, u)\}_\circ \text{mgu}_4 = \{P(A, A, A), P(A, u, A), P(A, u, u)\}\)

  • \(D_4 = \{A, u\}\)

  • \(\Delta \text{mgu} = \{A/u\}\)

  • \(\text{mgu}_5 = \text{mgu}_{4\circ} \Delta \text{mgu} = \{A/x, A/w, A/z, A/y, A/u\}\)

  • \(k = 4 + 1 = 5\)

Pass #5

  • \(\{P(x, z, y), P(w, u, w), P(A, u, u)\}_\circ \text{mgu}_5 = \{P(A, A, A)\}\)

  • Stop.

Clauses

Clauses are WFFs consisting of disjunctions of literals e.g. \(P \lor Q \lor R\), \( P \lor Q \lor \sim R\) etc.

Any predicate calculus WFF can be converted into a set of clauses

Example: \((P \lor Q) \land (R \lor S) \)

A set of clauses = \(\{\{P, Q\}, \{R, S\}\}\)

Resolution

It is an important rule of inference.

It can be applied on a set of parent clauses to generate new clauses called resolvents.

Resolution can be applied on a pair of parent clauses if they contain at least a pair of complementary literals.

Example: Reslution on ground clauses

  • Parent clauses: \(P_1 \lor P_2 \lor \cdots \lor P_N\), \(\sim P_1 \lor Q_2 \lor \cdots \lor Q_M\)

  • Resolvent: \(P_2 \lor \cdots \lor P_N \lor Q_2 \lor \cdots \lor Q_M\)

Parent Clause Resolvent(s) Comment(s)

\(P\) and \(\sim P \lor Q (\equiv P \Rightarrow Q)\)

\(Q\)

Modus Ponens

\((P \lor Q)\) and \((\sim P \lor Q)\)

\(Q\)

The resolvent is called merge

\((P \lor Q)\) and \((\sim P \lor \sim Q)\)

\(Q \lor \sim Q, P \lor \sim P\)

Two possible resolvents are tautologies

\(P\) and \(\sim P\)

\(\text{NIL}\)

The empty clause is a sign of contradiction

\(\sim P \lor Q (\equiv P \Rightarrow Q)\) and \(\sim Q \lor R (\equiv Q \Rightarrow R)\)

\(\sim P \lor R \equiv (P \Rightarrow R)\)

Chaining

Soundness of Resolution

If the clauses \( \{ \lambda \} \cup \Sigma_1 \) and \( \{ \sim \lambda \} \cup \Sigma_2 \) both have value True under an interpretation, then their resolvent, \( \Sigma_1 \cup \Sigma_2 \) also has a value True under the same interpretation.

The above rule is a sound rule of inference.

Proof: Reasoning by Cases

Case 1: \(\lambda\) \(=\) True, then \(-\lambda\) \(=\) False

Then, the clause \(\Sigma_2\) must have value True in order for the clause \(\{ \lambda \} \cup \Sigma_2\) to be True.

Case 2: \(\lambda\) \(=\) False, then \(-\lambda\) \(=\) True

Then, the clause \(\Sigma_1\) must have value True in order for the clause \(\{ \lambda \} \cup \Sigma_1\) to be True.

Combining the two cases, we see that either \(\Sigma_1\) or \(\Sigma_2\) must have value True, hence the resolvent \(\Sigma_1 \cup \Sigma_2\) must also have value True.

Conversion from WFFs to Clauses

Any WFF in propositional calculus can be converted into an equivalent conjunction of clauses.

A WFF written as a conjunction of clauses is said to be in conjunctive normal form (CNF).

A WFF written as a disjunction of clauses is said to be in disjunctive normal form (DNF).

Steps

Steps for conversion of WFFs to clauses:

Consider the WFF \(\sim (P \Rightarrow Q) \lor (R \Rightarrow P)\)

  1. Eliminate implications e.g. \(P \Rightarrow Q \equiv \sim P \lor Q\)

  2. Reduce scope of negation symbols e.g. \(\sim (\forall x) P(x) \equiv (\exists x) \sim P(x)\), \(\sim (\exists x) P(x) \equiv (\forall x) \sim P(x)\)

  3. Standardize variables e.g. \((\forall x) P(x) \Rightarrow (\exists x) Q(x) \equiv (\forall x_1) P(x_1) \Rightarrow (\exists x_2) Q(x_2)\)

    Each quantifier will have its own variable

  4. Eliminate existential quantifiers e.g. replace \( (\exists x) P(x) \) with \(P(A)\) if \(x = A\) satisfies \(P(x)\)

    Replace \((\forall y) \{(\exists x) P(x, y)\}\) with \((\forall y)\{P(g(y), y)\}\)

    • \(g(y) \rightarrow\) Skolem function

  5. Convert the input WFF into prenex normal form by moving all \(\forall\)'s to the front of the WFF. The prenex normal form of a WFF minus the \(\forall\)'s is called a matrix.

  6. Put the matrix in conjunctive normal form (CNF) i.e. as conjunctions of disjunctions of literals e.g. \((P_1 \lor P_2 \lor P_3) \land (Q_1 \lor Q_2) \land (R_1 \lor R_2 \lor R_3)\)

    If necessary, apply \(X \lor (Y \land Z) = (X \lor Y) \land (X \lor Z)\)

  7. Eliminate universal quantifiers

  8. Eliminate '\(\land\)' symbols

  9. Rename variables e.g. \( (P(x) \lor Q(x)) \land (R(x) \lor W(x))\) \(=\) \(\{\{P(x_1), Q(x_1)\}, \{R(x_2), W(x_2)\}\}\)

  10. Stop

General Resolution

General resolution is applied on clauses containing variables.

Let \(L\) and \(M\) be a pair of parent clauses.

We find \(\{l_i, \dots\} \subseteq L\) and \(\{ m_i, \dots\} \subseteq M\) and an mgu, \(s\), such that \( ( \{ l_i, \dots \} \cup \{\sim m_i, \sim \dots\} )_\circ s \) reduces to a singleton set.

The resolvent is \( ( \{ L - \{l_i, \dots\} \} \cup \{ M - \{m_i, \dots\} \} )_\circ s \)

resolution generalized

Examples

In the following example, the parent clauses \( L \) and \( M \) are \( P(x) \lor Q(x) \) and \( \sim P(A) \lor R(B) \) respectively.

We select the subsets \(\{ l_i, \dots \} = \{ P(x) \}\) and \(\{ m_i, \dots \} = \{ \sim P(A) \}\).

Thus, in order to find the resolvent of \(P(x) \lor Q(x)\) and \(\sim P(A) \lor R(B)\), we unify \( \{ P(x), \sim \sim P(A)\} \) with an mgu.

resolution 01
Note
 The resolvent of two parent clauses \(L\) and \(M\) may not be unique. It depends on the choice of \(\{ l_i, \dots \}\) and \(\{ m_i, \dots \}\), and consequently, the choice of mgu. Consider the examples that follow.

Suppose we have parent clauses \(P(x) \lor Q(x)\) and \(\sim P(A) \lor \sim P(y) \lor R(B)\). Depending on the choice of subsets and the choice of mgu, the resolvent is found to be different.

Case 1: \(\{ l_i, \dots \} = \{ P(x) \}\) and \(\{ m_i, \dots \} = \{ \sim P(A) \}\)

resolution 02 1

Case 2: \(\{ l_i, \dots \} = \{ P(x) \}\) and \(\{ m_i, \dots \} = \{ \sim P(y) \}\)

resolution 02 2

Case 3: \(\{ l_i, \dots \} = \{ P(x) \}\) and \(\{ m_i, \dots \} = \{ \sim P(A) \lor \sim P(y) \}\)

resolution 02 3

A Prototype Resolution Refutation System

Let \(S\) be a set of WFFs (i.e. the set of axioms) and \(w\) be the WFF to be proved (i.e. theorem).

\(S \cup \{\sim w\} \rightarrow\) base set

Steps

  1. Convert \(S \cup \{ \sim w \} \) to a set of clauses

  2. Go on applying resolution out of \(S \cup \{ \sim w \} \cup \{ \text{derived clauses} \}\) until an empty clause is derived

  3. Stop

Example 1

\(w = \text{Used-for-Counting}(THREE)\)

\( (\forall x) [\text{Pos-Integer}(x) \Rightarrow \text{Natural-No}(x)] \)

\( \sim \text{Pos-Integer}(x) \lor \text{Natural-No}(x) \)

\( (\forall y) [\text{Natural-No}(y) \Rightarrow \text{Used-for-Counting}(y)] \)

\( \sim \text{Natural-No}(y) \lor \text{Used-for-Counting}(y) \)

The refutation tree is as follows:

refutation 01
Note
 Refutation tree may not be unique.

Example 2

Consider the following sentences

  1. Any whole number is an integer

    \( (\forall x) [\text{Whole-No}(x) \Rightarrow \text{Integer}(x)]\)

  2. Fractions are not integers

    \( (\forall y) [\sim \text{Fraction}(y) \lor \sim \text{Integer}(y)]\)

  3. Some fractions are positives

    \( (\exists u) [\text{Fraction}(u) \land \text{Positive}(u)]\)

Using resolution, we need to prove that: "Some positives are not whole numbers."

venn

The base set of clauses includes:

  • \( \sim \text{WN}(x) \lor \text{I}(x) \)

  • \( \sim F(y) \lor \sim I(y) \)

  • \(F(A)\)

  • \(P(A)\)

  • \(\sim P(z) \lor \sim WN(z)\)

The refutation tree is as follows:

refutation 02

Control Strategies for Resolution Refutation Systems

  • Breath first control

  • Set of supports

    • Unit preference

  • Linear input form

Breadth First Strategy

All of the first level resolvents are computed first, then the second level resolvents and so on

A first level resolvent is one between two clauses in the base set

An \(i\)th level resolvent is one between a clause in the base set and an \(i-1\)th level resolvent

It is complete, but grossly inefficient.

@TODO: insert graph of size of clause vs no. of levels in the refutation tree for breadth first

Set of Supports Strategy

One of the parent clauses is selected:

  • either from the negation of the goal WFF or

  • its descendants

The strategy is complete.

Compared to breadth first strategy, it produces fewer clauses at each level.

It results in slower growth rate of the clause set to help moderate the usual combinatorial explosion.

@TODO: insert graph of size of clause vs no. of levels in the refutation tree for set of supports

Unit Preference Strategy

It is a modified version of set of supports strategy

Every time, a single literal, called a unit, is selected to be a parent in a resolution.

It is complete and efficient.

Linear Input Form Strategy

At least one of the parent clauses must be selected from the base set i.e. \(S \cup \{ \sim w\} \)

It lacks completeness, but is simple and efficient.

@TODO: add illustration of linear input form strategy

Ancestry Filtered Form Strategy

One parent is selected from one of:

  • the base set or

  • an ancestor of the other parent

Completeness can be preserved if ancestors are limited to merges.

@TODO: add illustration of ancestry filtered form strategy

Combination of Control Strategies

Control strategies may be combined together for higher efficiency.

Set of supports + Linear input form

Set of supports + Ancestry filtered form

Resolutions do have effect on the efficiency.

The following factors may be considered for ordedring resolutions for making combined control strategies

  • Unit preference

  • The number of literals in a clause

  • The complexity of terms in a clause

Major Problems with Resolution Refutation Systems

If a WFF w is not a logical consequence of a set of WFFs \(\Delta\), i.e. \(\Delta \not\models w\), then the resolution refutation system might not terminate.

  • That is, predicate calculus is semi-decidable

Even on WFFs for which the resolution refutation procedure terminates, the problem is NP hard. That is, the time complexity of the proof finding algorithm grows exponentially with increase number of literals in the base set.

The scope for application of heuristics for making complex reasoning tractable is almost nil for the resolution refutation system.

Example: The way the English statements are worded often carries extra logical or heuristics, control information.

\[( \forall x)( \forall y) \{[ \text{Gt}(x, 0) \land \text{Gt}(y, 0) ] \Rightarrow \text{Gt} ( \text{times}(x, y), 0) \} \; - (\text{i}) \\ ( \forall x)( \forall y) \{[ \text{Gt} (\text{times}(x, y), 0) \land \sim \text{Gt}(y, 0) ] \Rightarrow \sim \text{Gt}(y, 0) \} \; - (\text{ii})\]

Both the WFFs have the same clausal form, \(\sim \text{Gt}(x, 0) \lor \sim \text{Gt}(y, 0) \lor \text{Gt}(\text{times}(x, y), 0)\)

Statement (i) seems to indicate that we are to use the fact that \(x\) and \(y\) are individually greater than 0 to prove that the product of \(x\) and \(y\) is greater than 0.

Making Reasoning Efficient

  • Forgo the soundness of inference rules (use algorithms that may occasionally "prove" an untrue formula)

  • Forgo completeness (use algorithms which are not guaranteed to find proofs of true formulas)

  • Use a language that is less expressive than full predicate calculus (e.g. one that uses Horn clauses)

  • Reasoning is typically more efficient with Horn clauses, sufficient for many applications

Reasoning with Horn Clauses

Horn clauses form the basis of the programming language, Prolog They function as the statements of the language.

Inference over prolog clauses consists of attempting to "prove" a goal clause

  • It is performed by executing a prolog program

    • Such a program is achieved by resolution-like operations performed over prolog facts, rules, and goals.

  • Each resolution is performed either:

    • between a goal and a rule, or

    • between a goal and a fact

@TODO: insert prolog resolution diagram

Horn Clauses

Horn clauses are defined by the following criteria:

  • they can have at most one positive literal

  • an implication of the form

    \[\lambda_{b_1} \land \lambda_{b_2} \land \cdots \land \lambda_{b_n} \Rightarrow \lambda_h\]

    is represented as

    \[\{ \sim \lambda_{b_1} \lor \lambda_{b_2} \lor \cdots \lor \lambda_{b_n} \lor \lambda_h \}\]

In prolog, Horn clauses are written as

\[\underbrace{\lambda_h}_{\text{head}} \text{:- } \underbrace{\lambda_{b_1}, \lambda_{b_2}, \dots, \lambda_{b_n}}_{\text{body}}\]
Horn Clause No. of Literals Represented As

Rule

One positive literal

\( \lambda_h \text{:- } \lambda_{b_1}, \lambda_{b_2}, \dots, \lambda_{b_n} \)

Fact

No negative literal

\( \lambda_h \text{:- } \)

Rule

No positive literal

\( \text{:- } \lambda_{b_1}, \lambda_{b_2}, \dots, \lambda_{b_n} \)

Example: Prolog Program

Let us write a prolog program for the following:

  1. Jack and John are classmates

  2. John and Jill are classmates

  3. Any two who are classmates are friends

  4. If \(x\) and \(z\) are classmates and \(z\) and \(y\) are friends, then \(x\) and \(y\) are friends

Prove that Jack and Jill are friends.

  1. Class-mate(Jack, John) :-

  2. Class-mate(John, Jill) :-

  3. Friend(u, v) :- Class-mate(u, v)

  4. Friend(x, y) :- Class-mate(x, z), Friend(z, y)

  5. :- Friend(Jack, Jill)

@TODO: insert prolog and-or tree diagram

The process is readily seen to be equivalent to ordinary linear resolution on clauses using a depth first backtracking search with ordering of resolution governed by the ordering of clauses and the and/or tree produced by the prolog interpreter.

← Previous: Simulated Annealing | ↑ Up: Advanced Artificial Intelligence | Next: Uncertainty Management →