Proof procedure
In
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
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
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
- Proof tableaux
- Deductive system
- Proof (truth)
References
- Willard Quine1982 (1950). Methods of Logic. Harvard Univ. Press.