Considering a simple example for a Knowledge base which states that a Professor is a Person which is an University Employee or a Person which is not a Student. If one want to deduce if a Professor is also a Person. Although this is quite obvious it is good to proof this in a formal way.
First given the Knowledge Base and the Assumption, one adds the negated Assumption (what we want to proof whether is a logical Consequence) to our Knowledge Base, so one transforms this into a Disjunction, negated that yield a Conjunction with the help of the De Morgans Law which is the negated Assumption. One instantiates this on an Individual, because on proposes that there must be an Individual that fulfills the negated Query. If it is not is, i.e. one detects a Contradiction, then one ones that there does not exists some Individual that fulfills this, because it was the Negation, the opposite holds. Thus it is proofed by Refutation.
P ... Professor
E ... Person
U ... University Employee
D ... Student
Knowledge Base: P ⊑ (E⊓U)⊔(E⊓¬D)
Is P ⊑ E a logical Consequence?
Knowledge Base W (with [negated; [Query](/blog/518/)) in NNF:
W:{¬P⊔)(E⊓U)⊔(E⊓¬D), (P⊓¬E)(a)}
Tableaux A:
(1) (P⊓¬E)(a) (from [Knowledge](/blog/691/) Base)
(2|α from 1) P(a)
(3|α from 1) ¬E(a)
(4) (¬P⊔(E⊓U)⊔(E⊓¬D))(a) (from [Knowledge](/blog/691/) Base)
(5|β from 4)) ¬P(a) | (6) ((E⊓U)⊔(E⊓¬D))(a)
(7|β from 6) (E⊓U)(a) | (8) (E⊓¬D)(a)
(9|α from 7) E(a)
(10|α from 8) E(a)
(11|α from 7) U(a)
(12|α from 8) ¬D(a)
All path are closed, therefore the original Assumption that a Professor is also a Person holds.
Knowledge Base: ¬Person ⊔ ∃hasParent.Person
infer: ¬Person(Bill) { ¬Person ⊔ ∃hasParent.Person, Person(Bill)}
¬Person ⊔ ∃hasParent.Person(Bill)
¬Person(Bill)
∃hasParent.Person(Bill)
hasParent(Bill,x1)
Person(x1)
(¬Person ⊔ ∃hasParent.Person)(x1)
¬Person(x1)
∃hasParent.Person(x1)
hasParent(x1,x2)
Person(x2)
(¬Person ⊔ ∃hasParent.Person)(x2)
¬Person(x2)
∃hasParent.Person(x2)
No Termination possible
Problem with existential quantification