Spring ‘22 AI Homework 6: solutions
Let D be a domain consisting of individual animals, species, and time periods. Let L be the first-order language over D with the following primitives:
Animal(a) — Predicate. a is an animal.
SpeciesOf(a,s) — Predicate. Animal a belongs to species s.
Copyright By PowCoder代写 加微信 powcoder
Living(a,t) — Predicate. Animal a was alive at time t.
Extinct(s,t) — Predicate. Species s was extinct at time t.
Parent(p,c) — Predicate. Animal p is a parent of animal c.
RinTinTin, Dog, Mammoth, 1918 — Constants with the obvious meanings.
1. [2 pts.] 1.
Express the following statements in L
If p is a parent of c and c belongs to species s then p also belongs to species s. A species s is extinct at time t if and only if no animal belonging to s is alive at t. No mammoths were alive in 1918.
Mammoths were extinct in 1918.
Using resolution theorem proving, prove d. as a consequence of {b., c.}.
2. [8 pts.]
You must show the intermediate stages of Skolemization. You must show all the clauses
generated.
a. ∀p,c,s Parent(p,c) ^ SpeciesOf(c, s) => SpeciesOf(p, s)
b. ∀s,t Extinct(s, t) <=> ¬ ∃a [SpeciesOf(a, s) ^ Living(a,t)]
c. ¬∃a SpeciesOf(a, Mammoth) ^ Living(a, 1918)
d. Extinct(Mammoth, 1918)
Note: you could include Animal(p) ^ Animal(c) in a; Animal(a) in RHS of b. Fine either way. There were other ways to write ‘b’, although this may be “cleanest”.
2. To prove d as a consequence of {b,c} we add ¬d to out set of sentences, then convert to CNF and, then finally find a contradiction via proof.
Step 1: remove <=> (from b only)
∀s,t (Extinct(s, t) => ¬ ∃a [SpeciesOf(a, s) ^ Living(a,t)]) ^ (¬ ∃a [SpeciesOf(a, s) ^ Living(a,t)] => Extinct(s, t))
Step 2: remove => (again b only)
∀s,t (¬ Extinct(s, t) v ¬ ∃a [SpeciesOf(a, s) ^ Living(a,t)]) ^ (∃a [SpeciesOf(a, s) ^ Living(a,t)] v Extinct(s, t))
Step 3 push in ¬ (note how c becomes a universal)
b. ∀s,t (¬ Extinct(s, t) v ∀a ¬SpeciesOf(a, s) v ¬Living(a,t)]) ^ (∃a [SpeciesOf(a, s) ^ Living(a,t)] v Extinct(s, t))
c. ∀a ¬ SpeciesOf(a, Mammoth) v ¬ Living(a, 1918)
Skolemization: existential quantifier – a is scoped on s, t; same a appears in 2 places
b. ∀s,t (¬ Extinct(s, t) v ∀a ¬SpeciesOf(a, s) v ¬Living(a,t)]) ^ ([SpeciesOf(Sk0(s,t), s) ^ Living(Sk0(s,t),t)] v Extinct(s, t))
Skolemization: just remove universal
b. (¬ Extinct(s, t) v ¬SpeciesOf(a, s) v ¬Living(a,t)]) ^([SpeciesOf(Sk0(s,t), s) ^ Living(Sk0(s,t),t)] v Extinct(s, t))
c. ¬ SpeciesOf(a, Mammoth) v ¬ Living(a, 1918)
Distribute, add other clauses, pushing in ! makes c easy b-> 1,2,3; c->4 ; ¬d -> 5
# I number each CNF clause in the knowledge base so that each addition can be tracked.
1 ¬Extinct(s, t) v ¬SpeciesOf(a, s) v ¬Living(a,t) 2 SpeciesOf(Sk0(s,t), s) v Extinct(s, t)
3 Living(Sk0(s,t),t) v Extinct(s, t)
4 ¬SpeciesOf(a, Mammoth) v ¬Living(a, 1918) 5 ¬Extinct(Mammoth, 1918)
Resolve 5+2 {s -> Mammoth, t -> 1918}
6 SpeciesOf(Sk0(Mammoth,1918), Mammoth)
Resolve 6 + 4 {a->Sk0(Mammoth,1918)} 7 ¬Living(Sk0(Mammoth,1918), 1918)
Resolve 7 + 3 {s -> Mammoth, t -> 1918} 8 Extinct(Mammoth, 1918)
Resolve 5+8 to get the NULL clause. Proof complete.
The order of resolutions may be different and include other derived clauses.
Note how each step adds a clause to the KB (nothing ever gets removed).
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com