10  First-order Logic

10.1 Representation Revisited

Programming languages

Programming language is a kind of formal languages.

  • Programs represent computational processes while their data structures represent facts.
    • E.g., the Wumpus world can be represented by a 4\times4 array, “World[2,2] \gets Pit” states that “There is a pit in square [2,2].”
  • Lack of general mechanisms to derive facts from other facts
    • Update to a data structure is done by a domain-specific procedure.
  • Lack of expressiveness to handle partial information
    • E.g., to say “There is a pit in [2,2] or [3,1]”, a program stores a single value for each variable and allows the value to be “unknown”, while the propositional logic sentence, P_{2,2}\lor P_{1,1}, is more intuitive.

Propositional logic

  • Propositional logic is a declarative language.
    • Semantics is based on the truth relation between sentences and possible worlds.
  • Propositional logic allows partial/disjunctive/negated information
    • Unlike most data structures and databases
  • Propositional logic is compositional, which is desirable in representation languages
    • The meaning of a sentence is a function of the meaning of its parts; e.g., the meanings of S_{1,4}\land S_{1,2} relates the meanings of S_{1,4} and S_{1,2}.
  • Meaning in propositional logic is context-independent
    • Unlike natural language, where meaning depends on context
  • Propositional logic has very limited expressive power
    • E.g., cannot say “pits cause breezes in adjacent squares”

First-order logic

Whereas propositional logic assumes world contains facts, first-order logic (like natural language) assumes the world contains

  • Objects: are referred by nouns and noun phrases
    • E.g., people, houses, numbers, theories, Ronald McDonald, colors, baseball games, wars, centuries \ldots
  • Relations: can be unary relations (properties) or n-ary relations, representing by verbs and verb phrases
    • Properites: red, round, bogus, prime, multistoried, etc.
    • n-ary relations: brother of, bigger than, inside, part of, has color, occurred after, owns, comes between, etc.
  • Predicates: are relations that return true/false
  • Functions: are relations that return object

Logics in general

Language Ontological Commitment (What exists in the world) Epistemological Commitment (What an agent believes about facts)
Propositional logic facts true/false/unknown
First-order logic facts, objects, relations true/false/unknown
Temporal logic facts, objects, relations, time true/false/unknown
Probability logic facts degree of belief \in[0,1]
Fuzzy logic facts + degree of truth \in[0,1] known interval value

10.2 Syntax and Semantics

BNF Grammar

\begin{array}{rcl} Sentence & \to & AtomicSentence\mid ComplexSentence\\ AtomicSentence & \to & Predicate\mid Predicate(Term,...)\mid Term_{1}=Term_{2}\\ ComplexSentence & \to & (Sentence)\mid[Sentence]\\ & | & \lnot Sentence\\ & | & Sentence\land Sentence\\ & | & Sentence\lor Sentence\\ & | & Sentence\implies Sentence\\ & | & Sentence\iff Sentence\\ & | & Quantifier\:Variable,...Sentence\\ \\Term & \to & Function(Term,...)\\ & | & Constant\\ & | & Variable\\ \\Quantifier & \to & \forall\mid\exists\\ Constant & \to & A\mid X_{1}\mid John\mid...\\ {\color{red}Variable} & \to & {\color{red}a}\mid{\color{red}x}\mid{\color{red}s}\mid...\\ {\color{green}Predicate} & \to & {\color{green}True}\mid{\color{green}False}\mid{\color{green}After}\mid{\color{green}Loves}\mid{\color{green}Raining}\mid...\\ {\color{green}Function} & \to & {\color{green}mother}\mid{\color{green}leftleg}\mid...\\ \\\text{Operator Precedence} & : & \lnot,=,\land,\lor,\implies,\iff \end{array}

Terms

Term is a logical expression that refers to an object

  • Constants
  • Functions
  • Variables

Ground term is a term without variables

Graph representation of a model

  • A model can be represented as a directed graph.
  • The following graph contains five objects, two binary relations, three unary relations (indicated by labels on the objects), and one unary function, left-leg.

Models in First-order logic

A model m in first-order logic maps:

  • Constant symbols to objects m(R)=o_{1} and m(J)=o_{2}
  • Predicate/function symbols to tuples of objects

\begin{align*} m({\color{green}Person}) & =\{o_{1},o_{2}\} \\ m({\color{green}King}) & =\{o_{2}\} \\ m({\color{green}Crown}) & =\{o_{5}\} \\ m({\color{green}Brother}) & =\{(o_{1},o_{2}),(o_{2},o_{1})\} \\ m({\color{green}onhead}) & =\{(o_{5},o_{2})\} \\ m({\color{green}leftleg}) & =\{(o_{1},o_{3}),(o_{2},o_{4})\} \\ \end{align*}

  • Similar to propositional logic, entailment, validity, and so on are defined in terms of all possible models.

  • The number of possible models is unbounded \to checking entailment by the enumeration is infeasible.

  • 137,506,194,466 models with six or fewer objects.

A restriction on models

“Richard and John are people.”

{\color{green}Person}(Richard)\land{\color{green}Person}(John)

  • Unique names assumption: Each object has at most one constant symbol. This rules out m_{2}.
  • Domain closure: Each object has at least one constant symbol. This rules out m_{3}.

Point: contstant symbol \longleftrightarrow object

Quantifiers

Universal quantification

\forall\left\langle {\color{red}variables}\right\rangle \;\left\langle sentence\right\rangle

\forall{\color{red}x}\:P({\color{red}x}) is true in a model m iff P({\color{red}x}) is true with {\color{red}x} being each possible object in the model

  • Think conjunction: \forall{\color{red}x}\:P({\color{red}x}) is like P(A)\land P(B)\land\dots

Existential quantification

\exists\left\langle {\color{red}variables}\right\rangle \;\left\langle sentence\right\rangle

\exists{\color{red}x}\:P({\color{red}x}) is true in a model m iff P({\color{red}x}) is true with {\color{red}x} being some possible object in the model

  • Think disjunction: \exists{\color{red}x}\:P({\color{red}x}) is like P(A)\lor P(B)\lor\dots

Natural language quantifiers

  • “Everyone at Berkeley is smart”

    \forall{\color{red}x}\;\left({\color{green}At}({\color{red}x},Berkeley)\implies{\color{green}Smart}({\color{red}x})\right)

    equivalent to the conjunction of instantiations

    \begin{array}{cl} & ({\color{green}At}(King\,John,Berkeley)\implies{\color{green}Smart}(King\,John))\\ \land & ({\color{green}At}(Richard,Berkeley)\implies{\color{green}Smart}(Richard))\\ \land & ({\color{green}At}(Berkeley,Berkeley)\implies{\color{green}Smart}(Berkeley))\\ \land & \ldots \end{array}

  • “Someone at Stanford is smart”

    \exists{\color{red}x}\;\left({\color{green}At}({\color{red}x},Stanford)\land{\color{green}Smart}({\color{red}x})\right)

    equivalent to the disjunction of instantiations

    \begin{array}{cl} & ({\color{green}At}(King\,John,Berkeley)\land{\color{green}Smart}(King\,John))\\ \lor & ({\color{green}At}(Richard,Berkeley)\land{\color{green}Smart}(Richard))\\ \lor & ({\color{green}At}(Berkeley,Berkeley)\land{\color{green}Smart}(Berkeley))\\ \lor & \ldots \end{array}

A common mistake to avoid

  1. The main connective with \forall is \implies; mistake: using \land as the main connective with \forall

    \forall{\color{red}x}\;\left({\color{green}At}({\color{red}x},Berkeley)\land{\color{green}Smart}({\color{red}x})\right) means “Everyone is at Berkeley and everyone is smart” (too strong implication)

  2. The main connective with \exists is \land; mistake: using \implies as the main connective with \exists

    \exists{\color{red}x}\;\left({\color{green}At}({\color{red}x},Stanford)\implies{\color{green}Smart}({\color{red}x})\right) means “It is true even with anyone who is not at Stanford” (too weak implication)

Nested quantifiers

Multiple quantifiers enable more complex sentences. The order of quantification is therefore very important.

  • Simplest cases: Quantifiers are of the same type

    \forall{\color{red}x}\forall{\color{red}y}\:\left({\color{green}Brother}({\color{red}x},{\color{red}y})\implies{\color{green}Sibling}({\color{red}x},{\color{red}y})\right)

    \forall{\color{red}x}\forall{\color{red}y}\:\left({\color{green}Sibling}({\color{red}x},{\color{red}y})\iff{\color{green}Sibling}({\color{red}y},{\color{red}x})\right)

  • Mixtures

    \forall{\color{red}x}\exists{\color{red}y}\:{\color{green}Loves}({\color{red}x},{\color{red}y}) \to “Everybody loves somebody”

    \exists{\color{red}x}\forall{\color{red}y}\:{\color{green}Loves}({\color{red}x},{\color{red}y}) \to “There is someone loved by everyone”

Confusion: can arise when two quantifiers are used with the same variable name

\forall{\color{red}x}\:({\color{green}Crown}({\color{red}x})\lor(\exists{\color{red}x}\:{\color{green}Brother}(Richard,{\color{red}x})))

Rule:

  • The variable belongs to the innermost quantifier that mentions it or
  • Use different variable names with nested quantifier

\forall{\color{red}x}\:({\color{green}Crown}({\color{red}x})\lor(\exists{\color{red}z}\:{\color{green}Brother}(Richard,{\color{red}z})))

Properties of quantifiers

  • Nested quantifiers

\begin{array}{lcr} \forall{\color{red}x}\forall{\color{red}y}\:P({\color{red}x},{\color{red}y}) & \equiv & \forall{\color{red}y}\forall{\color{red}x}\:P({\color{red}x},{\color{red}y})\\ \exists{\color{red}x}\exists{\color{red}y}\:P({\color{red}x},{\color{red}y}) & \equiv & \exists{\color{red}y}\exists{\color{red}x}\:P({\color{red}x},{\color{red}y})\\ \exists{\color{red}x}\forall{\color{red}y}\:P({\color{red}x},{\color{red}y}) & \not\equiv & \forall{\color{red}y}\exists{\color{red}x}\:P({\color{red}x},{\color{red}y}) \end{array}

  • De Morgan’s rules

\begin{array}{rcl} \forall{\color{red}x}\:\lnot P({\color{red}x}) & \equiv & \lnot\exists{\color{red}x}\:P({\color{red}x})\\ \lnot\forall{\color{red}x}\:P({\color{red}x}) & \equiv & \exists{\color{red}x}\:\lnot P({\color{red}x})\\ \forall{\color{red}x}\:P({\color{red}x}) & \equiv & \lnot\exists{\color{red}x}\:\lnot P({\color{red}x})\\ \lnot\exists{\color{red}x}\:\lnot P({\color{red}x}) & \equiv & \exists{\color{red}x}\:P({\color{red}x}) \end{array}

Equality

  • term_{1}=term_{2} is true under a given interpretation if and only if term_{1} and term_{2} refer to the same object
  • \lnot(term_{1}=term_{2}) means term_{1} and term_{2} not refer to the same object (sometimes write as term_{1}\neq term_{2})
  • {\color{green}father}(John)=Henry means that {\color{green}father}(John) and Henry refer to the same object

Fun with sentences

  • Brothers are siblings \forall{\color{red}x},{\color{red}y}\;\left({\color{green}Brother}({\color{red}x},{\color{red}y})\implies{\color{green}Sibling}({\color{red}x},{\color{red}y})\right)
  • “Sibling” is symmetric \forall{\color{red}x},{\color{red}y}\;\left({\color{green}Sibling}({\color{red}x},{\color{red}y})\iff{\color{green}Sibling}({\color{red}y},{\color{red}x})\right)
  • One’s mother is one’s female parent \forall{\color{red}x},{\color{red}y}\;\left({\color{green}Mother}({\color{red}x},{\color{red}y})\iff({\color{green}Female}({\color{red}x})\land{\color{green}Parent}({\color{red}x},{\color{red}y}))\right)
  • A first cousin is a child of a parent’s sibling \forall{\color{red}x},{\color{red}y}\;\left({\color{green}FirstCousin}({\color{red}x},{\color{red}y})\iff\exists{\color{red}p},{\color{red}ps}\;\left({\color{green}Parent}({\color{red}p},{\color{red}x})\land{\color{green}Sibling}({\color{red}ps},{\color{red}p})\land{\color{green}Parent}({\color{red}ps},{\color{red}y})\right)\right)

10.3 Applications

Using First-Order Logic

First-order knowledge base KB has // interface

  • Sentences (assertions) are added to a knowledge base KB using \text{Tell}

    • \text{Tell}(KB,{\color{green}King}(John))
    • \text{Tell}(KB,{\color{green}Person}(Richard))
    • \text{Tell}(KB,\forall{\color{red}x}\:({\color{green}King}({\color{red}x})\implies{\color{green}Person}({\color{red}x})))

  • We can ask questions (queries or goals) of the knowledge base KB using \text{Ask}

    • \text{Ask}(KB,{\color{green}Person}(John)) \to return true
    • \text{Ask}(KB,\exists{\color{red}x}\:{\color{green}Person}({\color{red}x})) \to return true

  • If we want to know what value of {\color{red}x} makes the sentence true using \text{AskVars}

    • \text{AskVars}(KB,{\color{green}Person}({\color{red}x})) \to return a substitution list \left\{{\color{red}x}/John\right\} and \left\{{\color{red}x}/Richard\right\}

  • The assertions can be considered as the axioms

  • Logical sentences which are entailed by the axioms are called theorems

  • The theorems do not increase the set of conclusions that follow from the knowledge base KB

From a practical point of view, theorems are essential to reduce the computational cost of deriving new sentences

The Kinship Domain

  • Unary predicates
    • Male and Female
  • Binary predicates represent kinship relations
    • Parenthood, brotherhood, marriage, etc.
    • Parent, Sibling, Brother , Sister, Child, Daughter, Son, Spouse, Wife, Husband, Grandparent , Grandchild , Cousin, Aunt, and Uncle.
  • Functions
    • Mother and Father, each person has exactly one of each of these.

The Little Kinship Domain

The possible axioms for Kinship domain

  1. One’s mother is one’s female parent \forall m,c\,({\color{green}mother}(c)=m\iff{\color{green}Female}(m)\land{\color{green}Parent}(m,c)).
  2. One’s husband is one’s male spouse \forall w,h\,({\color{green}Husband}(h,w)\iff{\color{green}Male}(h)\land{\color{green}Spouse}(h,w)).
  3. Male and female are disjoint categories \forall x\,({\color{green}Male}(x)\iff\lnot{\color{green}Female}(x)).
  4. Parent and child are inverse relations \forall p,c\,({\color{green}Parent}(p,c)\iff{\color{green}Child}(c,p)).
  5. A grandparent is a parent of one’s parent \forall g,c\,({\color{green}GrandParent}(g,c)\iff\exists p\;{\color{green}Parent}(g,p)\land{\color{green}Parent}(p,c)).
  6. A sibling is another child of one’s parents \forall x,y\,({\color{green}Sibling}(x,y)\iff x\neq y\land\exists p\;{\color{green}Parent}(p,x)\land{\color{green}Parent}(p,y)).

Using axioms to entail theorems

\text{axioms of kinship}\models\forall x\forall y\:({\color{green}Sibling}(x,y)\iff{\color{green}Sibling}(y,x))

Natural number theory

  • To present the theory of natural numbers, we need
    • a predicate {\color{green}NatNum} that will be true of natural numbers
    • one constant symbol, 0
    • one function symbol, {\color{green}s} (successor)
    • one addition function, \mathbin{\color{green}+}
  • The Peano axioms define natural numbers and addition. Natural numbers are defined recursively
    1. {\color{green}NatNum}(0)
    2. \forall n\,({\color{green}NatNum}(n)\implies{\color{green}NatNum}(S(n)))
    3. \forall n\,(0\neq{\color{green}s}(n))
    4. \forall m,n\,(m\neq n\implies{\color{green}s}(m)\neq{\color{green}s}(n))
    5. \forall m\,(0\neq{\color{green}NatNum}(m)\implies\mathbin{\color{green}+}(0,m)=m)
    6. \forall m,n\,({\color{green}NatNum}(m)\land{\color{green}NatNum}(n)\implies\mathbin{\color{green}+}({\color{green}s}(m),n)={\color{green}s}(\mathbin{\color{green}+}(m,n)))

Set theory

  • The domain of sets is also fundamental to mathematics as well as to commonsense reasoning
  • We need
    • The empty set is a constant written as \emptyset
    • The unary predicate, {\color{green}Set}, which is true of sets.
    • The infix binary predicate x\in s (x is a member of set s)
    • The infix binary predicate s_{1}\subseteq s_{2} (set s_{1} is a subset of set s_{2})
    • The infix binary function s_{1}\cap s_{2} (the intersection of two sets)
    • The infix binary function s_{1}\cup s_{2} (the union of two sets)
    • The binary function $ $ (the set resulting from adjoining element x to set s)

One possible set of axioms is as follows

  1. The only sets are the empty set and those made by adjoining something to a set \forall s\,\left({\color{green}Set}(s)\iff\left(s=\emptyset\right)\lor\left(\exists x,s_{2}\,{\color{green}Set}(s_{2})\land s=\left\{ x\mid s_{2}\right\} \right)\right)

  2. The empty set has no elements adjoined into it. In other words, there is no way to decompose \emptyset into a smaller set and an element \lnot\exists x,s\;\left\{ x\mid s\right\} =\emptyset.

  3. Adjoining an element already in the set has no effect \forall x,s\;x\in s\iff s=\left\{ x\mid s\right\} .

  4. The only members of a set are the elements that were adjoined into it. We express this recursively, saying that x is a member of s if and only if s is equal to some set s_{2} adjoined with some element y, where either y is the same as x or x is a member of s_{2} \forall x,s\;\left(x\in s\iff\exists y,s_{2}\left(s=\left\{ y\mid s_{2}\right\} \land\left(x=y\lor x\in s_{2}\right)\right)\right).

  5. A set s_{1} is a subset of another set s_{2} if and only if all of the first set’s members are members of the second set \forall s_{1},s_{2}\,\left(s_{1}\subseteq s_{2}\iff(\forall x\;x\in s_{1}\Rightarrow x\in s_{2})\right).

  6. Two sets s_{1} and s_{2} are equal if and only if each is a subset of the other \forall s_{1},s_{2}\,\left(s_{1}=s_{2}\iff(s_{1}\subseteq s_{2}\land s_{2}\subseteq s_{1})\right).

  7. An object x is in the intersection of two sets s_{1} and s_{2} if and only if it is a member of both sets \forall x,s_{1},s_{2}\,\left(x\in(s_{1}\cap s_{2})\iff(x\in s_{1}\land x\in s_{2})\right).

  8. An object x is in the union of two sets s_{1} and s_{2} if and only if it is a member of either set \forall x,s_{1},s_{2}\,\left(x\in(s_{1}\cup s_{2})\iff(x\in s_{1}\lor x\in s_{2})\right).

Knowledge base for the wumpus world

  • The corresponding first-order sentence stored in the knowledge base must include both the percept and the time t at which it occurred
  • The actions in the wumpus world are also represented by logical terms

Agent

  • Perception:

    • Percept([s,b,g,m,c],t),Stench(t),Breeze(t),Glitter(t)
    • \text{Tell}(KB,\forall t,s,g,m,c \;Percept\left([s,Breeze,g,m,c],t\right)\implies Breeze(t))
    • \text{Tell}(KB,\forall t,s,b,m,c \;Percept\left([s,b,Glitter,m,c],t\right)\implies Glitter(t))
    • \text{Tell}(KB,Percept([Stench,Breeze,Glitter,None,None],5))

  • Action:

    • TurnRight,TurnLeft,Forward,Shoot,Grab,Climb,BestAction
    • For simple “reflex” behavior \text{Tell}(KB,\forall t\:(Glitter(t)\implies BestAction(Grab,t)))
    • To determine which is best, the agent program executes the query \text{AskVars}(KB,\exists a\:BestAction(a,t))

Environment

\begin{array}{l} \text{Tell}(KB,\forall x,y,a,b\:(Adjacent([x,y],[a,b])\iff \\ (x=a\land(y=b-1\lor y=b+1))\lor(y=b\land(x=a-1\lor x=a+1)))) \end{array}

\text{Tell}(KB,\forall x,s_{1},s_{2},t\:(At(x,s_{1},t)\land At(x,s_{2},t)\implies s_{1}=s_2))

\text{Tell}(KB,\forall s,t\:(At(Agent,s,t)\land Breeze(t)\implies Breezy(s)))

\text{Tell}(KB,\forall s\:(Breezy(s)\iff\exists r\:Adjacent(r,s)\land Pit(r)))

10.4 Simple Inference

A brief history of reasoning

450B.C. Stoics
322B.C. Aristotle
1965 Robinson

Substitution

A substitution \theta is a mapping from variables to terms. \text{Subst}[\theta,\alpha] returns the result of performing substitution \theta on \alpha. Note that: \text{Subst}[\theta,\alpha] also written as \alpha\theta.

  • \text{Subst}(\ \{{\color{red}x}/alice\},{\color{green}P}({\color{red}x}))={\color{green}P}(alice)
  • \text{Subst}(\ \{{\color{red}x}/alice,{\color{red}y}/{\color{red}z}\},{\color{green}P}({\color{red}x})\land{\color{green}Q}({\color{red}x},{\color{red}y}))={\color{green}P}(alice)\land{\color{green}Q}(alice,{\color{red}z})

Skolem normal form

A sentence of first-order logic is in Skolem normal form if it is written as a string of quantifiers and variables (with only universal first-order quantifiers) followed by a quantifier-free part.

  • Every first-order sentence may be converted into Skolem normal form while not changing its satisfiability.

Universal instantiation (UI)

Every instantiation of a universally quantified sentence is entailed by it \frac{\forall{\color{red}x}\\ \alpha}{\text{Subst}(\ \{{\color{red}x}/g\},\alpha)} for any variable {\color{red}x} and ground term g (a term without variables)

\begin{align*} & \forall{\color{red}x}\:({\color{green}King}({\color{red}x})\land{\color{green}Greedy}({\color{red}x})\implies{\color{green}Evil}({\color{red}x}))\models\\ & King\text{-}John\land Greedy\text{-}John\implies Evil\text{-}John\\ & King\text{-}Richard\land Greedy\text{-}Richard\implies Evil\text{-}Richard\\ & King\text{-}Father\text{-}John\land Greedy\text{-}Father\text{-}John\implies Evil\text{-}Father\text{-}John \end{align*}

Existential instantiation (EI)

For any sentence \alpha, variable {\color{red}x}, and constant symbol k (skolem constant) that does not appear elsewhere in the knowledge base \frac{\exists{\color{red}x}\\ \alpha}{\text{Subst}(\ \{{\color{red}x}/k\},\alpha)}

\exists{\color{red}x}\:({\color{green}Crown}({\color{red}x})\land{\color{green}OnHead}({\color{red}x},John))\models{\color{green}Crown}(C_{1})\land{\color{green}OnHead}(C_{1},John) provided C_{1} is a new constant symbol

  • The logic equivalence \forall{\color{red}x}\,\exists{\color{red}y}\,{\color{green}R}({\color{red}x},{\color{red}y})\Longleftrightarrow\exists{\color{red}y}\,\forall{\color{red}x}\,{\color{green}R}({\color{red}x},{\color{green}f}({\color{red}x})) where {\color{green}f}({\color{red}x}) is a function that maps {\color{red}x} to {\color{red}y}.

For any sentence \alpha, variable {\color{red}x},{\color{red}y}, and and function {\color{green}f} (skolem function) \frac{\forall{\color{red}x}\,\exists{\color{red}y}\,\alpha}{\text{Subst}(\ \{{\color{red}y}/{\color{green}f}({\color{red}x})\},\alpha)}

UI vs. EI

  • UI can be applied several times to add new sentences; the new KB is logically equivalent to the old
  • EI can be applied once to replace the existential sentence; the new KB is not equivalent to the old, but it can be shown to be inferentially equivalent (the new KB is satisfiable iff the old KB was satisfiable)

Propositionalization

  • Knowledge base KB in first-order logic

    \begin{array}{l} {\color{green}King}(John)\\ {\color{green}Greedy}(John)\\ {\color{green}Brother}(Richard,John).\forall{\color{red}x}\:({\color{green}King}({\color{red}x})\land{\color{green}Greedy}({\color{red}x})\implies{\color{green}Evil}({\color{red}x})) \end{array}

\downarrow\;\text{(Instantiating)}

  • Knowledge base in propositional logic

    \begin{array}{l} King\text{-}John\\ Greedy\text{-}John\\ Brother\text{-}Richard\text{-}John\\ King\text{-}John\land Greedy\text{-}John\implies Evil\text{-}John\\ King\text{-}Richard\land Greedy\text{-}Richard\implies Evil\text{-}Richard \end{array}

  • Claim: A ground sentence is entailed by new KB iff entailed by original KB

  • Claim: Every FOL KB can be propositionalized so as to preserve entailment

  • Idea: Propositionalize KB and query, apply resolution, return result

  • Problem: with function symbols, there are infinitely many ground terms,

    • E.g., {\color{green}father}({\color{green}father}({\color{green}father}(John)))

Theorem (Herbrand, 1930)

If a sentence \alpha is entailed by an FOL KB, it is entailed by a finite subset of the propositionalization of KB

  • Idea:

    for n = 0 to ∞ do
    create a propositional KB by instantiating with
    depth-n terms see if α is entailed by this KB

  • Problem: works if \alpha is entailed, loops if \alpha is not entailed

Theorem (Turing, 1936; Church, 1936)

Entailment in FOL is semidecidable

  • Algorithms exist that say yes to every entailed sentence, but no algorithm exists that also says no to every non-entailed sentence.

Problems with propositionalization

  • Propositionalization seems to generate lots of irrelevant sentences. For example,

    \begin{align*} & {\color{green}King}(John)\\ & {\color{green}Brother}(Richard,John)\\ & \forall{\color{red}x}\:{\color{green}Greedy}({\color{red}x})\\ & \forall{\color{red}x}\:({\color{green}King}({\color{red}x})\land{\color{green}Greedy}({\color{red}x})\implies{\color{green}Evil}({\color{red}x})) \end{align*}

    it seems obvious that Evil\text{-}John, but propositionalization produces lots of facts such as Greedy\text{-}Richard that are irrelevant

  • With p k-ary predicates and n constants, there are p\cdot n^{k} instantiations

  • With function symbols, it gets nuch much worse!

10.5 Unification

Unification

Unification is a process to find substitutions \theta that make different logical expressions p and q look identical. \text{Unify}(p,q)=\theta where \text{Subst}(\theta,p)=\text{Subst}(\theta,q)

p q \theta
{\color{green}Knows}(John,{\color{red}x}) {\color{green}Knows}(John,Jane) \{{\color{red}x}/Jane\}
{\color{green}Knows}(John,{\color{red}x}) {\color{green}Knows}({\color{red}y},Mary) \{{\color{red}x}/Mary,{\color{red}y}/John\}
{\color{green}Knows}(John,{\color{red}x}) {\color{green}Knows}({\color{red}y},{\color{green}mother}({\color{red}y})) \{{\color{red}y}/John,{\color{red}x}/{\color{green}mother}(John)\}
{\color{green}Knows}(John,{\color{red}x}) {\color{green}Knows}({\color{red}x},Mary) fail

Most General Unifier (MGU)

  • Consider the unification \text{Unify}({\color{green}Knows}(John,{\color{red}x}),{\color{green}Knows}({\color{red}y},{\color{red}z})), the results could be
    • \theta_{1}=\{{\color{red}y}/John,{\color{red}x}/z\}
    • \theta_{2}=\{{\color{red}y}/John,{\color{red}x}/John,{\color{red}z}/John\} The first unifier \theta_{1} is more general than the second \theta_{2}
  • There is a single Most General Unifier (MGU) that is unique up to renaming of variables \theta_{MGU}=\{{\color{red}y}/John,{\color{red}x}/{\color{red}z}\}

The unification algorithm

function Unify(s1, s2, θ) returns a substitution to make s1 and s2 identical

inputs: s1, a variable, constant, list, or compound
        s2, a variable, constant, list, or compound
        θ, the substitution built up so far (optional, defaults to empty)

    if θ = failure then 
        return failure
    else if s1 = s2 then 
        return θ
    else if Variable?(s1) 
        then return Unify-Var(s1, s2, θ)
    else if Variable?(s2) 
        then return Unify-Var(s2, s1, θ)
    else if Compound?(s1) and Compound?(s2) 
        then return Unify(s1.Args, s2.Args, Unify(s1.Op, s2.Op, θ))
    else if List?(s1) and List?(s2) then 
        return Unify(s1.Rest, s2.rest, Unify(s1.First, s2.First, θ))
    else return failure

function Unify-Var(var, s, θ) returns a substitution

    if {var/val} in θ then return Unify(val, s, θ)
    else if {s/val} in θ then return Unify(var, val, θ)
    else if Occur-Check?(var, s) then return failure
    else return add {var/s} to θ

Occur Check

  • Given \text{Unify-Var}({\color{red}var}, s) return failure if where {\color{red}var} occurs in s and s is not a variable
  • For example, \text{Unify-Var}({\color{red}x}, {\color{green}father}({\color{red}x})) cannot be unified.

Quiz: Unification

p q \theta
{\color{green}P}({\color{green}f}(A),{\color{green}g}({\color{red}x})) {\color{green}P}({\color{red}y},{\color{red}y})
{\color{green}P}(A,{\color{red}x},{\color{green}h}({\color{green}g}({\color{red}z}))) {\color{green}P}({\color{red}z},{\color{green}h}({\color{red}y}),{\color{green}h}({\color{red}y}))
{\color{green}P}({\color{red}x},{\color{green}f}({\color{red}x}),{\color{red}z}) {\color{green}P}({\color{green}g}({\color{red}y}),{\color{green}f}({\color{green}g}(B)),{\color{red}y})
{\color{green}P}({\color{red}x},{\color{green}f}({\color{red}x})) {\color{green}P}({\color{green}f}({\color{red}y}),{\color{red}y})
{\color{green}P}({\color{red}x},{\color{green}f}({\color{red}z})) {\color{green}P}({\color{green}f}({\color{red}y}),{\color{red}y})

10.6 Forward Chaining

First-order definite clauses

  • A definite clause is a disjunctions of literals of which exactly one is positive. It is
    • an atomic or
    • an implication whose antecedent is a conjunctions of positive literals and consequent is a positive literal
  • A first-order literal can include variables, which are assumed to be universally quantified

\begin{array}{l} {\color{green}King}({\color{red}x})\land{\color{green}Greedy}({\color{red}x})\Rightarrow{\color{green}Evil}({\color{red}x})\\ {\color{green}King}(John)\\ {\color{green}Greedy}({\color{red}y}) \end{array}

  • Datalog = first-order definite clauses + no functions

Generalized Modus Ponens (GMP)

Generalized Modus Ponens For atomic sentences p_{i}, p_{i}^{\prime}, and q, where there is a substitution \theta such that \text{Subst}(\theta,p_{i}^{\prime})=\text{Subst}(\theta,p_{i}), for all i \dfrac{p_{1}^{\prime},p_{2}^{\prime},...,p_{n}^{\prime},\left(p_{1}\land p_{2}\land...\land p_{n}\Rightarrow q\right)}{\text{Subst}(\theta,q)}

For example

p_{1}^{\prime} is {\color{green}King}(John) p_{1} is {\color{green}King}({\color{red}x})
p_{2}^{\prime} is {\color{green}Greedy}({\color{red}y}) p_{2} is {\color{green}Greedy}({\color{red}x})
q is {\color{green}Evil}({\color{red}x})
\theta is \left\{ {\color{red}x}/John,{\color{red}y}/John\right\} \text{Subst}(\theta,q) is Evil\text{-}John

Soundness of GMP

Lemma

For any definite clause p, we have p\models p\theta by UI

Proof Need to show that p_{1}^{\prime},\ldots,p_{n}^{\prime},(p_{1}\land\ldots\land p_{n}\Rightarrow q)\models q\theta provided that p_{i}^{\prime}\theta=p_{i}\theta for all i

  1. (p_{1}\land\ldots\land p_{n}\Rightarrow q)\models(p_{1}\land\ldots\land p_{n}\Rightarrow q)\theta=(p_{1}\theta\land\ldots\land p_{n}\theta\Rightarrow q\theta)
  2. p_{1}^{\prime},\ldots,p_{n}^{\prime}\models p_{1}^{\prime}\land\ldots\land p_{n}^{\prime}\models p_{1}^{\prime}\theta\land\ldots\land p_{n}^{\prime}\theta
  3. From 1 and 2, q\theta follows by ordinary Modus Ponens

Example 1

Problem

The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.

Prove that Colonel West is a criminal?

  • … it is a crime for an American to sell weapons to hostile nations

{\color{green}American}({\color{red}x})\land{\color{green}Weapon}({\color{red}y})\land{\color{green}Sells}({\color{red}x},{\color{red}y},{\color{red}z})\land{\color{green}Hostile}({\color{red}z})\implies{\color{green}Criminal}({\color{red}x})

  • Nono … has some missiles

{\color{green}Owns}(Nono,{\color{red}x})\land{\color{green}Missile}({\color{red}x})

  • … all of its missiles were sold to it by Colonel West

    {\color{green}Missile}({\color{red}x})\land{\color{green}Owns}(Nono,{\color{red}x})\implies{\color{green}Sells}(West,{\color{red}x},Nono)

  • Missiles are weapons

    {\color{green}Missile}({\color{red}x})\implies{\color{green}Weapon}({\color{red}x})

  • An enemy of America counts as “hostile”

    {\color{green}Enemy}({\color{red}x},America)\implies{\color{green}Hostile}({\color{red}x})

  • West, who is American …

    {\color{green}American}(West)

  • The country Nono, an enemy of America …

    {\color{green}Enemy}(Nono,America)

  • … and Colonel West is American

    {\color{green}American}(West)

Forward chaining algorithm

function FOL-FC-Ask(KB, α) returns a substitution or false

    repeat
        new ← ⌀

        for each rule in KB do
            (p1 ∧ … ∧ pn ⇒ q) ← Standardize-Variables(rule)

            for each substitution θ such that
                for all i, Subst(θ, pi) unifies with some fact in KB do

                q′ ← Subst(θ, q)

                if no sentence in KB ∪ new unifies with q′ then
                    add q′ to new

                    φ ← Unify(q′, α)
                    if φ ≠ fail then
                        return φ

        add all sentences in new to KB
    until new = ⌀

    return false

Forward chaining proof

Example 2

Problem

  • Art is the father of Bob and Bud.
  • Bob is the father of Cal and Coe.
  • Grandfather is the father of a father.

Question Is Art the grandfather of Coe?

Convert English sentences into FOL sentences

# FOL sentence explain
1 {\color{green}F}(Art,Bob) KB
2 {\color{green}F}(Art,Bud) KB
3 {\color{green}F}(Bob,Cal) KB
4 {\color{green}F}(Bob,Coe) KB
5 {\color{green}F}({\color{red}x},{\color{red}y})\land{\color{green}F}({\color{red}y},{\color{red}z})\implies{\color{green}G}({\color{red}x},{\color{red}z}) KB
6 {\color{green}G}(Art,Coe) 1,4,5 \left\{{\color{red}x}/Art,{\color{red}y}/Bob,{\color{red}z}/Coe\right\}

Properties of forward chaining

  • Sound:
    • YES, every inference is just an application of GMP
  • Complete:
    • YES for definite clause knowledge bases
    • It answers every query whose answers are entailed by any KB of definite clauses
  • It terminates for Datalog in poly iterations: at most p\cdot n^{k} literals
  • It may not terminate in general if \alpha is not entailed
    • This is unavoidable: entailment with definite clauses is semidecidable

Efficiency of forward chaining

  • Simple observation: no need to match a rule on iteration k if a premise wasn’t added on iteration k-1 \to match each rule whose premise contains a newly added literal
  • Matching itself can be expensive
  • Database indexing allows O(1) retrieval of known facts E.g., query {\color{green}Missile}({\color{red}x}) retrieves {\color{green}Missile}(M_{1})
  • Matching conjunctive premises against known facts is NP-hard
  • Forward chaining is widely used in deductive databases

Definite clauses with function symbols

  • Inference can explode forward and may never terminate.
  • Consider the following KB with two predicates and two functions

\begin{array}{l} {\color{green}Even}(2)\\ {\color{green}Even}({\color{red}x})\implies{\color{green}Even}({\color{green}plus}({\color{red}x},2))\\ {\color{green}Integer}({\color{red}x})\implies{\color{green}Even}({\color{green}times}({\color{red}x},2))\\ {\color{green}Even}({\color{red}x})\implies{\color{green}Integer}({\color{red}x}) \end{array}

Quiz: Forward chaining

  • Given a KB containing the following sentence

    {\color{green}Parent}({\color{red}x},{\color{red}y})\land{\color{green}Male}({\color{red}x})\implies{\color{green}Father}({\color{red}x},{\color{red}y})

    {\color{green}Father}({\color{red}x},{\color{red}y})\land{\color{green}Father}({\color{red}x},{\color{red}z})\implies{\color{green}Sibling}({\color{red}y},{\color{red}z})

    {\color{green}Male}(Tom)

    {\color{green}Parent}(Tom,John)

    {\color{green}Parent}(Tom,Fred)

  • Perform the forward chaining until a fixed point is reached.

10.7 Backward Chaining

A backward-chaining algorithm

function FOL-BC-Ask(KB, query) returns a generator of substitutions
    return FOL-BC-Or(KB, query, {})

generator FOL-BC-Or(KB, goal, θ) yields a substitution
    for each rule (lhs ⇒ rhs) in Fetch-Rules-For-Goal(KB, goal) do
        (lhs, rhs) ← Standardize-Variables((lhs, rhs))
        θ1 ← Unify(rhs, goal, θ)
        if θ1 ≠ failure then
            for each θ2 in FOL-BC-And(KB, lhs, θ1) do
                yield θ2

generator FOL-BC-And(KB, goals, θ) yields a substitution
    if θ = failure then return
    else if goals is empty then
        yield θ
    else
        first ← First(goals)
        rest ← Rest(goals)
        for each θ1 in FOL-BC-Or(KB, Subst(θ, first), θ) do
            for each θ2 in FOL-BC-And(KB, Subst(θ1, rest), θ1) do
                yield θ2

Backward chaining example

Properties of backward chaining

  • Depth-first recursive proof search
    • space is linear in size of proof
  • Incomplete due to infinite loops
    • fix by checking current goal against every goal on stack
  • Inefficient due to repeated subgoals (both success and failure)
    • fix using caching of previous results (extra space!)
  • Widely used for logic programming

10.8 Resolution

Conversion to CNF

A sentence “Everyone who loves all animals is loved by someone” is represented by

\forall{\color{red}x}[[\forall{\color{red}y}[{\color{green}Animal}({\color{red}y})\implies{\color{green}Loves}({\color{red}x},{\color{red}y})]]\implies[\exists{\color{red}z}\:{\color{green}Loves}({\color{red}z},{\color{red}x})]]

  1. Standardize variables: each quantifier should use a different one

    \forall{\color{red}x}[[\forall{\color{red}y}[{\color{green}Animal}({\color{red}y})\implies{\color{green}Loves}({\color{red}x},{\color{red}y})]]\implies[\exists{\color{red}z}\:{\color{green}Loves}({\color{red}z},{\color{red}x})]]

  2. Eliminate biconditionals and implications

    \forall{\color{red}x}[[\lnot\forall{\color{red}y}\:[\lnot{\color{green}Animal}({\color{red}y})\lor{\color{green}Loves}({\color{red}x},{\color{red}y})]]\lor[\exists{\color{red}z}\:{\color{green}Loves}({\color{red}z},{\color{red}x})]]

  3. Move \lnot inwards:

    \begin{array}{l} \forall{\color{red}x}[[\exists{\color{red}y}\:\lnot(\lnot{\color{green}Animal}({\color{red}y})\lor{\color{green}Loves}({\color{red}x},{\color{red}y}))]\lor[\exists z\:{\color{green}Loves}({\color{red}z},{\color{red}x})]] \\ \forall{\color{red}x}[[\exists{\color{red}y}\:(\lnot\lnot{\color{green}Animal}({\color{red}y})\land\lnot{\color{green}Loves}({\color{red}x},{\color{red}y}))]\lor[\exists z\:{\color{green}Loves}({\color{red}z},{\color{red}x})]] \\ \forall{\color{red}x}[[\exists{\color{red}y}\:(\lnot{\color{green}Animal}({\color{red}y})\land\lnot{\color{green}Loves}({\color{red}x},{\color{red}y}))]\lor[\exists z\:{\color{green}Loves}({\color{red}z},{\color{red}x})]] \end{array}

  4. Skolemize: a more general form of existential instantiation. Each existential variable is replaced by a Skolem function of the enclosing universally quantified variables

    \forall{\color{red}x}[[{\color{green}Animal}({\color{green}F}({\color{red}x}))\land\lnot{\color{green}Loves}({\color{red}x},{\color{green}f}({\color{red}x}))]\lor{\color{green}Loves}({\color{green}g}({\color{red}x}),{\color{red}x})

  5. Drop universal quantifiers

    [{\color{green}Animal}({\color{green}f}({\color{red}x}))\land\lnot{\color{green}Loves}({\color{red}x},{\color{green}f}({\color{red}x}))]\lor{\color{green}Loves}({\color{green}g}({\color{red}x}),{\color{red}x})

  6. Distribute \land over \lor

    [{\color{green}Animal}({\color{green}f}({\color{red}x}))\lor{\color{green}Loves}({\color{green}g}({\color{red}x}),{\color{red}x})]\land[\lnot{\color{green}Loves}({\color{red}x},{\color{green}f}({\color{red}x}))\lor{\color{green}Loves}({\color{green}g}({\color{red}x}),{\color{red}x})]

Generalized Resolution

Full first-order version \begin{equation} \frac{\ell_{1}\lor\cdots\lor{\color{red}\ell_{i}}\lor\cdots\lor\ell_{k},\qquad m_{1}\lor\cdots\lor{\color{green}{\color{orange}m_{j}}}\lor\cdots\lor m_{n}}{(\ell_{1}\lor\cdots\lor\ell_{i-1}\lor\ell_{i+1}\lor\cdots\lor\ell_{k}\lor m_{1}\lor\cdots\lor m_{j-1}\lor m_{j+1}\lor\cdots\lor m_{n})\theta} \end{equation} where \text{Unify}({\color{red}\ell_{i}},\lnot{\color{green}{\color{orange}m_{j}}})=\theta.

\frac{\begin{array}{l} {\color{green}\lnot Rich}({\color{red}x})\lor{\color{green}Unhappy}({\color{red}x}),\qquad{\color{green}Rich}(Ken)\end{array}}{\begin{array}{l} {\color{green}Unhappy}(Ken)\end{array}} with \theta=\{{\color{red}x}/Ken\}

Solution to Example 1

Solution to Example 2

# FOL clause explain
1 {\color{green}F}(Art,Bob) KB
2 {\color{green}F}(Art,Bud) KB
3 {\color{green}F}(Bob,Cal) KB
4 {\color{green}F}(Bob,Coe) KB
5 \lnot{\color{green}F}({\color{red}x},{\color{red}y})\lor\lnot{\color{green}F}({\color{red}y},{\color{red}z})\lor{\color{green}G}({\color{red}x},{\color{red}z}) KB
6 \lnot{\color{green}G}(Art,Coe) \lnot\alpha
7 \lnot{\color{green}F}(Art,{\color{red}y})\lor\lnot{\color{green}F}({\color{red}y},Code) 5,6 \left\{{\color{red}x}/Art,{\color{red}z}/Coe\right\}
8 \lnot{\color{green}F}(Art,Bob) 4,7 \left\{{\color{red}y}/Bob\right\}
9 \emptyset 1,8

Example 3

Problem

Everyone who loves all animals is loved by someone. Anyone who kills an animal is loved by no one. Jack loves all animals. Either Jack or Curiosity killed the cat, who is named Tuna. Did Curiosity kill the cat?

Solution to Example 3

Extract simple sentences from the problem

  1. Everyone who loves animals is loved by someone.

  2. Anyone who kills an animal is loved by no one.

  3. Jack loves all animals.

  4. Either Jack or Curiosity killed the cat.

  5. The cat is named Tuna.

  6. Cats are animals.

  7. Did Curiosity kill the cat?

Convert to FOL sentences

  1. \forall{\color{red}x}[[\forall{\color{red}y}{\color{green}Animal}({\color{red}y})\implies{\color{green}Loves}({\color{red}x},{\color{red}y})]\implies\exists{\color{red}z}{\color{green}Loves}({\color{red}z},{\color{red}x})]

  2. \forall{\color{red}x}[[\exists{\color{red}y}{\color{green}Animal}({\color{red}y})\land{\color{green}Kills}({\color{red}x},{\color{red}y})]\implies\forall{\color{red}z}\lnot{\color{green}Loves}({\color{red}z},{\color{red}x})]

  3. \forall{\color{red}x}[{\color{green}Animal}({\color{red}x})\implies{\color{green}Loves}(Jack,{\color{red}x})]

  4. {\color{green}Kills}(Jack,Tuna)\lor{\color{green}Kills}(Curiosity,Tuna)

  5. {\color{green}Cat}(Tuna)

  6. \forall{\color{red}x}[{\color{green}Cat}({\color{red}x})\implies{\color{green}Animal}(x)]

  7. \lnot{\color{green}Kills}(Curiosity,Tuna)

Convert to CNF sentences

  1. {\color{green}Animal}({\color{green}F}({\color{red}x}))\lor{\color{green}Loves}({\color{green}G}({\color{red}x}),{\color{red}x})

  2. \lnot{\color{green}Loves}({\color{red}x},{\color{green}F}({\color{red}x}))\lor{\color{green}Loves}({\color{green}G}({\color{red}x}),{\color{red}x})

  3. \lnot{\color{green}Loves}({\color{red}x},{\color{red}y})\lor\lnot{\color{green}Animal}({\color{red}z})\lor\lnot{\color{green}Kills}({\color{red}x},{\color{red}z})

  4. \lnot{\color{green}Animal}({\color{red}x}) \lor {\color{green}Loves}(Jack,{\color{red}x})

  5. {\color{green}Kills}(Jack,Tuna)\lor{\color{green}Kills}(Curiousity,Tuna)

  6. {\color{green}Cat}(Tuna)

  7. \lnot{\color{green}Cat}({\color{red}x})\lor{\color{green}Animal}({\color{red}x})

  8. \lnot{\color{green}Kills}(Curiousity,Tuna)

Using resolution to prove that Curiosity killed the cat

Suppose Curiosity did not kill Tuna. We know that either Jack or Curiosity did; thus Jack must have. Now, Tuna is a cat and cats are animals, so Tuna is an animal. Because anyone who kills an animal is loved by no one, we know that no one loves Jack. On the other hand, Jack loves all animals, so someone loves him; so we have a contradiction. Therefore, Curiosity killed the cat.

Exercise

Given a KB of the following sentences

  • Anyone whom Mary loves is a football star.
  • Any student who does not pass does not play.
  • John is a student.
  • Any student who does not study does not pass.
  • Anyone who does not play is not a football star.

Prove that “If John does not study, Mary does not love John”

10.9 References