~/ learn/ comp-456/ cards/ Resolution refutation: proving theorems by contradiction
1 of 6

A clause set in Prolog/CNF style — the rule, the fact, and the negated goal

A clause set in Prolog/CNF style — the rule, the fact, and the negated goal

Answer

q :- p. p. :- q.

`q :- p.` is the Horn-clause form of the rule P→Q (clause {¬P, Q}); `p.` is the fact (clause {P}); and `:- q.` is the *goal* clause — a headless clause that Prolog reads as "refute q", i.e. the negated goal {¬Q}. Prolog's execution IS linear-input resolution over exactly these three clauses.

space flip · ← → navigate · esc to exit
NORMAL ~/memra/library/fbdd936d-d20f-4dca-b2ab-fed9af924091/flashcard utf-8 LF