Can be use substitution for existential elimination in Horn clause?

Asked Dec 28 '22 at 03:33

Active Dec 28 '22 at 03:33

Viewed 18 times

I have a question that when prove and use forward and backward reasoning or resolution ,that in the clause have exitential quantifier, so can I not to use skolemization for substiution then just put it its to rule base and prove its like any horn clauses?Like:

R1: A(x) ⇒ Q(x)

R2: ∃x A(x) ∧ E(x)

R3: E(Dog)

Prove : Q(Dog)

With Subst={x/Dog} => R3 with R2 so get new fact is: A(Dog) and A(Dog) with R1 have Q(Dog)?

asked Dec 28 '22 at 03:33

chews

The fact that from R3 we know that Dog is an E, does not imply that it is the same Dog that in R2 is also an A. – Mauro ALLEGRANZA Dec 28 '22 at 08:34
So x in R2 must replace by a constant?Like A(f(x) ∧ E(f(x)) – chews Dec 28 '22 at 13:32

Can be use substitution for existential elimination in Horn clause?

0 Answers0