Automatic proof ( English Automated Theorem Proving, ATP , as well as Automated deduction ) - proof , implemented in software . It is based on the apparatus of mathematical logic . The ideas of the theory of artificial intelligence are used . The proof process is based on the logic of propositions and the logic of predicates .
Due to the insolubility of even fairly simple theories, only semi- automatic human-machine proofs have practical application. Moreover, after full automation, the proof is called computation . It can only be fully automatic to verify the proof of theories more complicated (if you prepare it for this).
Content
Application
Currently, automatic proof of theorems in industry is mainly used in the development and verification of integrated circuits and software. After a division error was detected in Pentium processors , complex modules of floating point operations of modern microprocessors are developed with great care. The new processors from AMD , Intel and other companies use automatic proof of theorems to verify that division and other operations are performed correctly.
Microsoft uses an automatic proof of theorems Z3 to verify the code of the operating system Windows 7 and other software products [1] .
Examples
- Agda
- Coq
- Idris
- Mercury
- is a project of Russian scientists working at the University of Manchester (Great Britain), who has won the world championship among proof systems 11 times.
See also
- Withdrawal machine
- Expert system
Notes
- β Gwen SalaΓΌn, Bernhard SchΓ€tz. Formal Methods for Industrial Critical Systems: 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings. - Springer, 2011 .-- P. 5. - ISBN 9783642244308 .
Links
- On the automatic proof of theorems
- Deduction Automation System (CAD)
- SPASS: An Automated Theorem Prover for First-Order Logic with Equality
- Beklemishev Lev . FAQ: Computer evidence . postnauka.ru ( 05.20.2014 ).