6 points) Consider the following first-order predicate calculus statements, whic

Question

6 points) Consider the following first-order predicate calculus statements, which have already been written in Skolemized clause form. Write all pairs of clauses below that can resolve (there are 6 of them). If a pair resolves, give the resulting substitution given by unification along with the resolution. Note: I am not asking you to give a complete proof, just the result of one resolution at a time. a. inst(sk(?a), human) v mortal(sk0(?a)) b. inst(Socrates, human) c. ~mortal(?b) d. ~inst(?c,?d) e. inst(Socrates, 2e) f. -inst(?f, human) v-married(spouse-of(?f) v single(?0) g. married(spouse-of(Socrates)

Explanation / Answer

1. ~inst(Socrates, human)

~inst(?c, ?d) => c= Socrates, d= human

2. ~inst(Socrates, human)

~inst(Socrates, ?e) => e = human

3. married(spouse-of(Socrates))

~inst(?f, human) V ~married(spouse-of(?f)) V single(?f) => f = Socrates

4. inst(sk(?a), human) V mortal(sk0(?a))

inst(Socrates, ?e) => a = Socrates, e = human

5. ~inst(Socrates, human)

inst(sk(?a), human) V mortal(sk0(?a)) => a = Socrates

6. inst(sk(?a), human) V mortal(sk0(?a))

inst(Socrates, ?e)

~mortal(?b)

a => Socrates, e = human, b = Socrates

Please let me know in case of any clarifications required. Thanks!

Related Questions

Navigate

• Browse (All)
• Browse 6
• Subjects

---

---

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.