Proof procedure
Wikipedia, the free encyclopedia - Cite This SourceIn logic, and in particular proof theory, a proof procedure is a method of proving statements. A statement p that is provable from a non-empty set Γ of statements in a theory K is called a deduction of p from Γ in K. If Γ is empty then p is either a theorem of K (i.e., ) or an axiom of K if K is axiomatic. We express that p is deducible (or provable or derivable or demonstrable) from Γ in K in symbols as
- .
There are several types of proof procedures. The most popular are natural deduction, sequent calculi (i.e., Gentzen type systems), Hilbert type axiomatic systems, and semantic tableaux or trees.
We call a proof procedure M for a theory K sound if each and every member of the set of deducible formulas is valid (with respect to the semantics of K). We say that M is complete if the set of deducible formulas is a superset of the set of valid formulas of K. (Generally this last statement regarding completeness states that M is complete if the set of deducible formulas is exactly the set of valid formulas of K. But proof procedures that prove, e.g., every formula, are trivially complete even if K is consistent. They are, however, unsound.)
See also
Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)
This article is licensed under the GNU Free Documentation License.
Last updated on Friday March 07, 2008 at 02:28:00 PST (GMT -0800)
View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation