Proof procedure
Encyclopedia
In logic
, and in particular proof theory
, a proof procedure for a given 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 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).
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, and in particular proof theory
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, a proof procedure for a given logic is a systematic method for producing proofs in some proof calculus
Proof calculus
In mathematical logic, a proof calculus corresponds to a family of formal systems that use a common style of formal inference for its inference rules...
of (provable) statements.
There are several types of proof calculi. The most popular are natural deduction
Natural deduction
In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...
, sequent calculi
Sequent calculus
In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as a tool for studying natural deduction in...
(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).
See also
- Automated theorem provingAutomated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
- Proof complexityProof complexityIn computer science, proof complexity is a measure of efficiency of automated theorem proving methods that is based on the size of the proofs they produce. The methods for proving contradiction in propositional logic are the most analyzed...
- Proof tableaux
- Deductive systemDeductive systemA deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the system....
- Proof (truth)Proof (truth)A proof is sufficient evidence or argument for the truth of a proposition.The concept arises in a variety of areas, with both the nature of the evidence or justification and the criteria for sufficiency being area-dependent...