 Refutation

A refutation of a collection of logical assumptions is a derivation of a contradiction from them. To prove a logical formula $\phi$ by refutation in classical propositional logic, add its negation $\neg \phi$ to the assumptions and derive falsity. The correctness of this inference follows from the rules of the chosen proof system.

For example, the clauses $p\vee q$, $\neg p$ and $\neg q$ have a resolution refutation: the first two resolve to $q$, and $q$ with $\neg q$ yields the empty clause. No truth assignment satisfies the three original clauses. This distinguishes the semantic claim of unsatisfiability from a syntactic certificate establishing it. In automated proving, producing a refutation is useful because another program can check the individual inference steps without repeating the search.