Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:theorem_prover [2008/02/20 10:31] vkuncak |
sav08:theorem_prover [2008/02/21 09:47] (current) vkuncak |
||
---|---|---|---|
Line 25: | Line 25: | ||
Example: | Example: | ||
* [[Isabelle Theorem Prover]] | * [[Isabelle Theorem Prover]] | ||
- | * [[http://pauillac.inria.fr/coq/|Coq Proof Assistant]] | + | * [[http://pauillac.inria.fr/coq/|Coq Proof Assistant]] - popular in programming languages community |
- | * [[http://www.cs.utexas.edu/~moore/acl2/|ACL2 Language and Prover]] | + | * [[http://www.cs.utexas.edu/~moore/acl2/|ACL2 Language and Prover]] - identifies a LISP subset with a logic |
=== Decision Procedure === | === Decision Procedure === | ||
- | It considers a smaller set of formulas, it always terminates and (given enough time) never says "I don't know". | + | Decision procedure considers a smaller set of formulas, it always terminates and (given enough time) never says "I don't know". |
Example decidable classes of formulas: | Example decidable classes of formulas: |