Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:theorem_prover [2008/02/20 10:30] vkuncak |
sav08:theorem_prover [2008/02/21 09:47] 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: | ||
| Line 43: | Line 43: | ||
| * Example: first-order logic | * Example: first-order logic | ||
| - | **Important question**: combining different decision procedures and using them inside provers. | + | **Important question**: combining different decision procedures and using them inside provers |
| + | * we will explore this question as well in this course | ||
| === Prover in Analysis === | === Prover in Analysis === | ||