Lecture
Automated theorem proving (also known as ATP or automated deduction) — is a subfield of automated reasoning and mathematical logic concerned with proving mathematical theorems by means of computer programs. The automation of reasoning over mathematical proofs has been an important stimulus for the development of computer science.
Automated theorem proving (ATP) is a field of artificial intelligence and mathematics concerned with developing computer programs or systems capable of automatically generating formal proofs for mathematical theorems.
The goal of ATP is to create algorithms and methods that can efficiently and reliably prove theorems in various mathematical fields, including logic, algebra, analysis, number theory and others.
Automated theorem proving is usually based on the formalization of mathematical theories and inference rules within a computer system. The system then applies logical reasoning, verification algorithms and transformations of statements in order to automatically construct proofs for given assertions or to refute them.
Possible methods used in automated theorem proving include resolution, direct methods, truth-table methods, inference mechanisms based on artificial neural networks, and others. Formal languages and verification systems are also used to formalize and check proofs.
Although the roots of formalized logic go back to Aristotle, modern logic and formalized mathematics developed at the end of the 19th and beginning of the 20th century. Frege's Begriffsschrift (1879) introduced both a complete propositional calculus and what is essentially , modern predicate logic. His «Grundlagen der Arithmetik» , published in 1884, expressed (in part) mathematics in formal logic. This approach was continued by Russell and Whitehead in their influential Principia Mathematica , first published in 1910–1913 and with a revised second edition in 1927. Russell and Whitehead thought that they could derive the whole of mathematical truth using axioms and rules of inference of formal logic, in principle opening up the process for automation. In 1920 Thoralf Skolem simplified an earlier result of Leopold Löwenheim, which led to the Löwenheim–Skolem theorem, and in 1930, to the notion of the Herbrand universe and Herbrand interpretation, which allowed the (un)satisfiability of first-order formulas (and hence the validity of a theorem) to be reduced to (potentially infinitely many) propositional satisfiability problems.
In 1929 Mojżesz Presburger showed that the theory of natural numbers with addition and equality (now called Presburger arithmetic in his honor) is decidable, and gave an algorithm that could determine whether a given sentence in the language was true or false. However, soon after this positive result Kurt Gödel published «On Formally Undecidable Propositions of Principia Mathematica and Related Systems» (1931), showing that in any sufficiently strong axiomatic system there are true statements that cannot be proved within the system. This topic was further developed in the 1930s by Alonzo Church and Alan Turing, who on the one hand gave two independent but equivalent definitions of computability, and on the other provided concrete examples of undecidable questions.
Soon after the Second World War, the first general-purpose computers appeared. In 1954 Martin Davis programmed Presburger's algorithm for the JOHNNIAC vacuum-tube computer at the Institute for Advanced Study in Princeton, New Jersey. According to Davis, «its great triumph was proving that the sum of two even numbers is even». More ambitious was the Logic Theory Machine in 1956, a deduction system for the propositional logic of Principia Mathematica , developed by Allen Newell, Herbert A. Simon and J. C. Shaw.. Also running on JOHNNIAC, the Logic Theory Machine constructed proofs from a small set of propositional axioms and three rules of inference: modus ponens , (propositional) substitution of variables, and replacement of formulas by their definitions. The system used heuristic guidance and managed to prove 38 of the first 52 theorems of Principia .
«Heuristic» approach of the Logic Theory Machine tried to imitate human mathematicians and could not guarantee that a proof could be found for every valid theorem, even in principle. In contrast, other, more systematic algorithms achieved, at least in theory, completeness for first-order logic. The initial approaches relied on the results of Herbrand and Skolem for converting a first-order formula into successively growing sets of propositional formulas by instantiating variables with terms from the Herbrand universe. The propositional formulas could then be checked for unsatisfiability using a number of methods. Gilmore's program used conversion into disjunctive normal form, a form in which the satisfiability of a formula is obvious
Depending on the underlying logic, the problem of determining the validity of a formula ranges from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but co-NP-complete, and hence it is believed that for general proof problems only algorithms with exponential running time exist. For first-order predicate calculus, Gödel's completeness theorem states that theorems (provable statements) are exactly the logically valid well-formed formulas, so the identification of valid formulas is recursively enumerable: given unlimited resources, any valid formula can eventually be proved. However, invalid formulas (those that do not follow from a given theory) cannot always be recognized as such.
The above applies to first-order theories such as Peano arithmetic. However, for a specific model that can be described by a first-order theory, some statements may be true but undecidable in the theory used to describe the model. For example, by Gödel's incompleteness theorem, we know that any theory whose own axioms are true for the natural numbers cannot prove the truth of all first-order statements about the natural numbers, even if the list of its own axioms can be enumerated infinitely. It follows that an automated theorem prover will fail to halt while searching for a proof exactly when the statement under investigation is undecidable in the theory being used, even if it is true in the model of interest. Despite this theoretical limit, in practice theorem provers can solve many complex problems, even in models that are not fully described by any first-order theory (for example, the integers).
A simpler but related problem is proof checking , in which an existing proof of a theorem is recognized as valid. This usually requires that each individual step of the proof can be checked by a primitive recursive function or program, and hence the problem is always decidable.
Because the proofs generated by automated theorem provers are usually very large, the problem of proof compression is of critical importance, and various methods have been developed aimed at making the prover's output smaller and hence more understandable and verifiable.
Proof assistants require a human user to give hints to the system. Depending on the degree of automation, a prover can essentially be reduced to a proof checker, with the user supplying the proof in a formal way, or important verification tasks may be carried out automatically. Interactive provers are used for a wide variety of tasks, but even fully automatic systems have proved a number of interesting and difficult theorems, including at least one that had long eluded human mathematicians, namely the Robbins conjecture. [10] [11] However, these successes are isolated, and working on complex problems generally requires an experienced user.
Another distinction is sometimes drawn between theorem proving and other methods, whereby a process is considered theorem proving if it consists of a traditional proof, starting from axioms and producing new inference steps using rules of inference. Other methods may include model checking , which in the simplest case involves brute-force enumeration of many possible states (although the actual implementation of model checkers requires a great deal of ingenuity and is not reducible to simple brute-force enumeration).
There are hybrid theorem-proving systems that use model checking as a rule of inference. There are also programs that have been written to prove a specific theorem, with a (usually informal) proof that if the program terminates with a certain result, then the theorem is true. A good example of this was the machine proof of the four color theorem , which was very controversial because the first claimed mathematical proof was practically impossible for humans to verify due to the enormous volume of computation performed by the program (such proofs are called unfalsifiable-refutable proofs ). Another example of a proof by program is one that shows that in the game « Connect Four» the first player can always win.
Commercial use of automated theorem proving is mainly concentrated in the design and verification of integrated circuits . After the Pentium FDIV bug, the complex floating-point units of modern microprocessors have been designed with particular care. AMD , Intel and others use automated theorem proving to ensure that division and other operations are correctly implemented in their processors.
Automated theorem proving has a wide range of applications, including the verification of software and hardware, checking the correctness of mathematical statements, the analysis of systems and security protocols, the development of formal languages, and others.
However, automated theorem proving remains the object of active research, and not all mathematical theorems can currently be proved fully automatically. Many problems require human intervention, intuition and creativity in order to find and formulate proofs.
In the late 1960s, agencies funding research in automated deduction began to emphasize the need for practical applications. One of the first fruitful areas was program verification , in which first-order theorem provers were applied to the problem of checking the correctness of computer programs written in languages such as Pascal, Ada, and so on. Among the first program-verification systems, notable was the Stanford Pascal Verifier. developed by David Luckham of Stanford University . [ 12] [13] [14] It was based on the Stanford Resolution Prover, also developed at Stanford using John Alan Robinson's resolution principle. This was the first automated deduction system that demonstrated the ability to solve mathematical problems that were announced in the Notices of the American Mathematical Society before the solutions were formally published. [ citation needed ]
First-order theorem proving — one of the most mature branches of automated theorem proving. The logic is expressive enough to allow arbitrary problems to be described, often in a fairly natural and intuitive way. On the other hand, it is still semi-decidable, and a number of sound and complete calculi have been developed that allow systems to be fully automated. [15] More expressive logics, such as higher-order logic , allow a wider range of problems to be conveniently expressed than first-order logic, but theorem proving for these logics is less well developed. [16] [17]
The quality of implemented systems has improved thanks to the existence of a large library of standard test problems — the «Thousands of Problems for Theorem Provers» problem library (TPTP) [18] — and also the annual CADE ATP System Competition (CASC). a competition of first-order systems for many important classes of first-order problems.
Some important systems (all of which have won at least one competitive division of CASC) are listed below.
The Theorem Proving Museum is an initiative to preserve the sources of theorem-proving systems for future analysis, since they are important cultural/scientific artifacts. It holds the sources of many of the systems mentioned above.
Comments