Automated Theorem Proving Tools
by: Lilly Irani
Though Automated Theorem Proving seems to imply computer independence from the use, ATP still functions supported by heuristics. Heuristics consist of a human interacting with computer, guiding the computer to "guesses" as to which proof technique or method to pursue. Thus, all of the following tools have interactive features to allow human-computer interaction.
from: Knuth, Donald E., "Mathematics and Computer Science: Coping with Finiteness." Science. 12/17/76
The Stanford Validity Checker (SVC) allows researchers to check if certain formulas are valid using a subset of first-order-logic. A subset is used because it has been shown that first-order-logic, as a whole, is undecideable.
The Stanford Temporal Prover (STeP) is a formal verification tool designed to help verify reactive, real-time systems. The STeP research team is led by Stanford Professor Zohar Manna.
To try demonstrations of STeP and see what sample logic problems and code syntax look like, go to STeP-related Online Demos.
Otter is a resolution system developed at Argonne National Laboratories. According to "Generic Automatic Proof Tools" by Lawrence C. Paulson, "they achieve extremely high inference rates and can run continuously for days without running out of storage. They can crack many of the toughest challenge problem that have been circulated." Otter relies on many specialized algorithms but it especially relies on unification to solve first order logic problems with equality.
For a fun, interactive demonstration of the theorem prover working, check out Son Of Birdbrain.