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.