08. Inference in First Order Logic Flashcards
Universal instantiation: we can …
We denote the result of applying the substitution θ to the sentence α by Subst(θ, α) so that
∀vα Subst({v /g }, α)
({v/g} means that v is replaced by g).
Above substitutions: {x/John}, {x/Richard}, {x/Father(John)}.
infer any sentence from substituting a ground term (a term without variables) for the variable.
When existential quantifiers appear, we…
More formally: For any sentence α, variable v, and constant symbol k that does not appear elsewhere in the knowledge base:
replace a variable by a single new constant symbol.
Existential Instantiation: Change of Knowledge Base
Universal Instantiation
Universal instantiation can be applied several times to add sentences. The new knowledge base is logically equivalent to the …
Existential Instantiation
Existential instantiation can be applied once to replace the existential sentence.
The new knowledge base is not …, but is satisfiable if the old knowledge base was satisfiable.
old when performing all possible substitutions and deleting the quantified sentence, or adding new sentences and keeping the quantified sentence.
equivalent to the old (more than one satisfying object might exist)
Reduction to Propositional Inference: General Approach
review slide 9: what should i understand from this important slide?
Problems with Propositionalization
Propositionalization seems to generate lots of irrelevant sentences. E.g., from
∀x King(x)∧Greedy(x)⇒Evil(x) King (John)
∀ y Greedy (y )
it seems obvious that Evil(John), but propositionalization …
With p k-ary predicates and n constants, there are
produces lots of facts such as Greedy(Richard) that are irrelevant.
p*n^k instantiations. With function symbols, it gets much worse!
What is Generalized Modus Ponens?
Due to the presented problems with propositionalization, we aim at directly inferring sentences in first-order logic.
To infer Evil(John) from a simplified version of the previous example
∀x King(x)∧Greedy(x)⇒Evil(x) King (John)
Greedy (John)
we only need to find a substitution θ that makes King(x), Greedy(x) identical to sentences already in the KB, so that we can assert the conclusion Evil(x).
Solution: θ = {x/John}.
(see slide 13 for example)
Unification
Lifted inference rules require …, called unification.
The unify algorithm Unify(p, q) = θ returns a unifier θ such that …
Remark:
Why do we standardize apart one of the two sentences by renaming its variables?
finding substitutions that make different logical expressions look identical
Subst(θ, p) = Subst(θ, q) if it exists.
If several unifications are used, they are considered to be taken in parallel, i.e. the order in which the substitutions are given does not matter.
–> because x cannot take the values John and Elizabeth at the same time.
Unification: Most General Unifier
In many cases, there is more than one unifier, e.g., Unify(Knows(John,x),Knows(y,z))
could return
{y/John,x/z} or {y/John,x/John,z/John}.
The first unifier gives …, the second one gives Knows(John,John). The second result can be obtained from the first one by the substitution z/John
→ The first unifier is more general.
There always exists a …
Knows(John,z) as the result
most general unifier as shown by the algorithm in Fig. 1 of the AI book in the section “Inference in First-Order Logic”.
Properties of Forward Chaining
Sound and complete for first-order Horn clauses
(proof similar to the one for propositional logic)
Forward chaining may not…; e.g., Peano axiom for natural numbers:
NatNum(0)
∀n NatNum(n) ⇒ NatNum(S(n)) (S(n) : successor of n)
Forward chaining would add NatNum(S(0)), NatNum(S(S(0))), … This is unavoidable: entailment with Horn clauses is semidecidable (as for general first-order logic).
Datalog: Declarative logic programming language
Datalog = first-order Horn clauses + no functions (e.g., crime KB) Forward chaining terminates for Datalog in a polynomial number of iterations: at most p · nk literals (p: number of predicates, k: maximum arity of predicates, n: number of constant symbols)
terminate in general if function symbols are involved
review Forward Chaining videos
Explain backward chaining.
Go through pseudocode on slides by yourself–> put it on paper
