Computer-assisted proof

Machine -assisted proofs (or ambiguous: automatic proofs, a branch of automatic deduction ) based on the use of computer programs for generation and verification of mathematical proofs of logical theorems. In contrast to a computer proof is attempted to construct the entire formal proof consisting of steps and intermediate results.

• 2.1 method
• 2.2 problems and theoretical limitations
• 2.3 Automatic Theorem Prover
• 2.4 Interactive Theorem Prover

Computer evidence

Method

We use the word in particular for evidence, which have the following scheme: First, it is shown that the general problem P is true if another property P is true, so if P can be reduced to e. It is crucial that E a finite number of ( usually very many ) cases can be decided by enumerating. The reduction of P on E is usually a regular, informal mathematical proof. Only in the next step, the computer comes into play: You write a program that enumerates all cases ( generate) and then checked in each case, whether it actually applies E (test). In fact, E is thus decided by a brute- force method. From both parts then the assertion follows P.

Objections to computer evidence

Computer evidence is controversial partly among mathematicians. In addition to more psychological or hypothetical objections, this phenomenon also very tangible methodical.

• A psychological objection is the ideal of a short, logical reasoning, which can be easily understood by everyone. Such evidence is, however, becoming increasingly rare in mathematical practice. The monsters evidence of current mathematical research can be of a single human being no longer understood in all parts (including the used lemmas ).
• Rather hypothetical objection is that the compiler or the hardware might have an error. Through repetitions on different computers and in different implementations of this risk can be minimized as required.
• Methodologically problematic is the question of whether the program implements the underlying algorithm correctly determine whether the algorithm in the generate- phase enumerates all cases, and the test- phase assuring actually the property E for this case. So there is a program verification problem.

Machine -assisted proofs

Method

It is a formalized mathematical proof, i.e., included in a sequence of logical steps single broken that they can be reconstructed by a computer program. Test evidence is a universal, only logic -dependent problem, while " generate- and- test" algorithms are problem-specific. There are therefore good reasons why to trust machines tested formal proofs more than computer evidence.

Problems and theoretical limitations

The question of whether a formal proof of each theorem can be constructed in a given logic is called decision problem. Depending on the underlying logic of the decision problem may vary from the trivial to the unsolvable. In the case of propositional logic, the problem is decidable (that is, a proof is always generated when the theorem is logically valid, otherwise the invalidity is detected ), but NP -complete. In contrast, first-order logic is only semi- decidable, that is, using unlimited time and memory resources can prove a valid theorem, an invalid, however, not always be recognized as such. Higher order logic (HOL ) is neither decidable nor (in terms of so-called standard models ) completely.

Automatic theorem Prover

Despite these theoretical limits practically usable automatic theorem provers ( ATPs ) have been implemented that can solve many difficult problems in these logics.

While theorem provers to derive evidence of theorems from axioms about Inferenzschritte and simulate mathematical proofs in any form, are used in the model verification ( model checking ) implemented mostly refined techniques used to enumerate brute -force proof states and systematically search search spaces of proof states. Some systems are also hybrids that use both interactive proof method and model checking.

Interactive theorem provers

A simpler but related problem is the proof verification, is where checked for a given formal proof, if it indeed proves a given theorem. For this purpose, only each individual proof step has to be checked, which is possible by simple functions normally.

Interactive theorem, also called proof assistants, require Advice for proof search, which must be given by a human user the proof system. Depending on the degree of automation can be a theorem essentially be reduced to a proof auditor or automatically perform independently significant parts of the proof search. Interactive theorem provers are now used for various tasks, the scope of pure mathematics in theoretical computer science extends to practical problems of program verification.

Scientific and industrial applications

Significant mathematical proofs, which were checked by interactive theorem prover, the proof of the four - color theorem by Georges Gonthier are ( the older computer proof by Appel and Haken replaces ) and the (currently unfinished ) formalized proof of Kepler 's conjecture by the flyspeck project. But automatic theorem prover now have to solve some interesting and difficult problems whose solution in mathematics was a long time unknown. However, such successes are sporadic, the processing of difficult problems usually requires interactive theorem prover.

Currently still the industrial use of theorem provers or model auditors focuses mainly on the verification of integrated circuits and processors. Since then errors with serious economic impact in commercial processors have become known (see Pentium FDIV bug), their processing units usually verified. In the latest processor versions of AMD, Intel and other theorem prover and model checker has been used to prove many critical operations in them. Lately theorem are also increasingly used for software verification; large projects include the part - verification of Microsoft's Hyper- V or an extensive verification of the L4 ( microkernel ).

Available implementations

Available implementations for automated theorem provers are eg Simplify, Z3 or Alt- Ergo, based on predicate logic.

Available implementations for interactive theorem prover Isabelle and Coq are using higher level logics (HOL or CC).

Examples of proof techniques

• Resolution
• Term Rewriting
• Model checking
• Induction
• Binary decision diagrams