Automated Theorem Proving and Formal Methods
Further information: First-order theorem provingAutomated theorem proving refers to the development of computer programs that search and find derivations (formal proofs) of mathematical theorems. Finding derivations is a difficult task because the search space can be very large; an exhaustive search of every possible derivation is theoretically possible but computationally infeasible for many systems of interest in mathematics. Thus complicated heuristic functions are developed to attempt to find a derivation in less time than a blind search.
The related area of automated proof verification uses computer programs to check that human-created proofs are correct. Unlike complicated automated theorem provers, verification systems may be small enough that their correctness can be checked both by hand and through automated software verification. This validation of the proof verifier is needed to give confidence that any derivation labeled as "correct" is actually correct.
Some proof verifiers, such as Metamath, insist on having a complete derivation as input. Others, such as Mizar and Isabelle, take a well-formatted proof sketch (which may still be very long and detailed) and fill in the missing pieces by doing simple proof searches or applying known decision procedures: the resulting derivation is then verified by a small, core "kernel". Many such systems are primarily intended for interactive use by human mathematicians: these are known as proof assistants. They may also use formal logics that are stronger than first-order logic, such as type theory. Because a full derivation of any nontrivial result in a first-order deductive system will be extremely long for a human to write, results are often formalized as a series of lemmas, for which derivations can be constructed separately.
Automated theorem provers are also used to implement formal verification in computer science. In this setting, theorem provers are used to verify the correctness of programs and of hardware such as processors with respect to a formal specification. Because such analysis is time-consuming and thus expensive, it is usually reserved for projects in which a malfunction would have grave human or financial consequences.
Read more about this topic: First-order Logic
Famous quotes containing the words automated, theorem, proving, formal and/or methods:
“Now, as always, the most automated appliance in a household is the mother.”
—Beverly Jones (b. 1927)
“To insure the adoration of a theorem for any length of time, faith is not enough, a police force is needed as well.”
—Albert Camus (1913–1960)
“The momentary charge at Balaklava, in obedience to a blundering command, proving what a perfect machine the soldier is, has, properly enough, been celebrated by a poet laureate; but the steady, and for the most part successful, charge of this man, for some years, against the legions of Slavery, in obedience to an infinitely higher command, is as much more memorable than that as an intelligent and conscientious man is superior to a machine. Do you think that that will go unsung?”
—Henry David Thoreau (1817–1862)
“This is no argument against teaching manners to the young. On the contrary, it is a fine old tradition that ought to be resurrected from its current mothballs and put to work...In fact, children are much more comfortable when they know the guide rules for handling the social amenities. It’s no more fun for a child to be introduced to a strange adult and have no idea what to say or do than it is for a grownup to go to a formal dinner and have no idea what fork to use.”
—Leontine Young (20th century)
“The reading public is intellectually adolescent at best, and it is obvious that what is called “significant literature” will only be sold to this public by exactly the same methods as are used to sell it toothpaste, cathartics and automobiles.”
—Raymond Chandler (1888–1959)