I'm trying to convert Solve a Resolution Refutation problem. The problem states: Knowledge Base is ∀ (, ). Prove using resolution-refutation that ∀ (, ). Note: β = F(y, x) This is what I think it might be:
Convert Clauses to CNF:
1 ∀xy F(x,y) -From KB
2 ∀x F(x,A(x))
3 F(x,A(x)) -CNF
Convert negation β to CNF:
1 ¬∀x F(A(x),x) -Negation of β
2 ∃x¬ F( A(x),x)
3 ¬ F( A(x),x) -CNF
Proof by Resolution-Refutation
1 F(x,A(x)) -From KB
2 ¬F( A(x),x) -Negation of β
3 Contradiction -Line 1 & 2
, respectively.
Table Format
Is that right? (For some reason the KB being F(x, y) and the Conclusion trying to prove F( y, x), it makes me think I'm missing something.) If not, could you explain to me what I'm missing? Thanks!