Proof procedure 1596638 217405104 2008-06-05T21:55:41Z SmackBot 433328 Date the maintenance tags or general fixes {{Unreferenced|date=June 2008}} In [[logic]], and in particular [[proof theory]], a '''proof procedure''' for a given [[logical system|logic]] is a systematic method for producing proofs in some [[proof calculus]] of (provable) statements. There are several types of proof calculi. The most popular are [[natural deduction]], [[sequent calculus|sequent calculi]] (i.e., Gentzen type systems), [[Hilbert type axiomatic system]]s, and [[semantic tableau]]x 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. A proof procedure for a logic is ''complete'' if it produces a proof for each provable ststement. The theorems of logical systems are typically [[recursively enumerable]], which implies the existence of a complete but 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 a [[semidecidable]] property, this is not possible, and instead the procedure will diverge (not terminate). ==See also== * [[Automated theorem proving]] * [[Proof complexity]] * [[Proof tableaux]] * [[Deductive system]] [[Category:Logic]] [[Category:Proof theory]] {{logic-stub}}