{{Short description|Systematic method for producing proofs}}
In logic, and in particular proof theory, a '''proof procedure''' for a given logic is a systematic method for producing proofs in some proof calculus of (provable) statements.
==Types of proof calculi used== There are several types of proof calculi. The most popular are natural deduction, sequent calculi (i.e., Gentzen-type systems), Hilbert systems, and semantic tableaux or trees. A given proof procedure will target a specific proof calculus, but can often be reformulated so as to produce proofs in other proof styles.
==Completeness== A proof procedure for a logic is ''complete'' if it produces a proof for each provable statement. The theorems of logical systems are typically recursively enumerable, which implies the existence of a complete but usually extremely inefficient proof procedure; however, a proof procedure is only of interest if it is reasonably efficient.
Faced with an unprovable statement, a complete proof procedure may sometimes succeed in detecting and signalling its unprovability. In the general case, where provability is only a semidecidable property, this is not possible, and instead the procedure will diverge (not terminate).
==See also== * Automated theorem proving * Proof complexity * Deductive system ==References== *Willard Quine 1982 (1950). ''Methods of Logic''. Harvard Univ. Press. Category:Proof theory