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: | ||