= Automated deduction
<Automated deduction> uses an <algorithm> to construct or check a <mathematical proof> from explicit assumptions and <inference rule>[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\lor 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 <predicate>[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.
Back to article page
