Express Knowledge base in CNF and resolution in prolog

user_8376187 0
Viewed 118

I have a knowledge base as CNF and i'd like to use prolog to make a resolution, but i can't wrap my head around how to formulate the problem in prolog.

I have

KB = { P v Q, Q => (R ^ S), (P v R) => U }

that i put in CNF as:

KB = { P v Q, not(Q) v R, not(Q) v S, not(P) v U, not(R) v U }

and i'd like to prove that KB entails U ( KB |= U ).

I can prove in manually by refutation but i'd like to know how this can be done using prolog ?

Thx

prolog
1 Answers

The answer is: it is impossible.

not(Q) v R, not(Q) v S, not(P) v U, not(R) v U

can be expressed by r:-q., s:-q., u:-p. and u:-r..

Questioning ? u. amounts to asking for a proof by refutation.

However,

P v Q

cannot be expressed as a fact/rule in a prolog program. Prolog is restricted to Horn clauses, i.e. disjunctions of literals that contain at most one positive literal.

user_65406060
Related