Proof Systems
Boyer-Moore Theorem Prover (NQTHM)
The design of this system was influenced by John McCarthy and Woody Bledsoe. Started in 1971 at Edinburgh, Scotland, this was a fully automatic theorem prover built using Pure Lisp. The main aspects of NQTHM were:
-
-
- 1. the use of Lisp as a working logic.
- 2. the reliance on a principle of definition for total recursive functions.
- 3. the extensive use of rewriting and "symbolic evaluation".
- 4. an induction heuristic based the failure of symbolic evaluation.
-
HOL Light
Written in Objective CAML, HOL Light is designed to have a simple and clean logical foundation and an uncluttered implementation. It is essentially another proof assistant for classical higher order logic.
Coq
Developed in France, Coq is another automated proof assistant, which can automatically extract executable programs from specifications, as either Objective CAML or Haskell source code. Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC).
Read more about this topic: Automated Reasoning
Famous quotes containing the words proof and/or systems:
“It comes to pass oft that a terrible oath, with a swaggering accent sharply twanged off, gives manhood more approbation than ever proof itself would have earned him.”
—William Shakespeare (1564–1616)
“The only people who treasure systems are those whom the whole truth evades, who want to catch it by the tail. A system is just like truth’s tail, but the truth is like a lizard. It will leave the tail in your hand and escape; it knows that it will soon grow another tail.”
—Ivan Sergeevich Turgenev (1818–1883)