Automated deduction

Automated deduction uses an algorithm to construct or check a mathematical proof from explicit assumptions and inference rules. The representation might use propositional logic, first-order logic or a specialized theory such as linear arithmetic. Soundness means the rules preserve truth; finding a proof additionally requires a search strategy.

For a small resolution example, the clauses $P\vee Q$, $\neg P$ and $\neg Q$ yield $Q$ and then the empty clause. This is a contradiction, so the original clauses cannot all hold. To prove a conclusion from assumptions, a refutation method adds its negation and searches for such a contradiction. In first-order logic, unification determines which terms can instantiate matching predicates. A procedure that eventually finds every valid proof need not terminate on every invalid claim: this distinction explains why proof search and proof checking have different computational costs.