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}}