|This article does not cite any references or sources. (June 2008)|
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.
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 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).
|This logic-related article is a stub. You can help Wikipedia by expanding it.|