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/18 16:55] vkuncak |
sav08:theorem_prover [2008/02/21 09:47] (current) vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
=== Notion of Automated Theorem Prover === | === Notion of Automated Theorem Prover === | ||
- | Theorem prover (TP) accepts a logical formula and tries to prove that the formula is valid. Possible outcomes: | + | Theorem prover (TP) accepts a //logical formula// and tries to prove that the formula is valid. Possible outcomes: |
* TP says: "Yes, formula is valid" | * TP says: "Yes, formula is valid" | ||
* TP says: "No, formula is not valid, here is a counterexample which shows it is false" | * TP says: "No, formula is not valid, here is a counterexample which shows it is false" | ||
Line 9: | Line 9: | ||
* TP loops forever | * TP loops forever | ||
- | Example theorem provers: | + | Example automated theorem provers: |
+ | * [[http://www.cs.nyu.edu/acsys/cvc3/|CVC3]] | ||
+ | * [[http://combination.cs.uiowa.edu/smtlib/|SMT-LIB Library and Competition]] | ||
* [[http://spass.mpi-sb.mpg.de/|SPASS]] from the Max Planck Institut for Computer Science | * [[http://spass.mpi-sb.mpg.de/|SPASS]] from the Max Planck Institut for Computer Science | ||
* [[http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html|E prover]] | * [[http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html|E prover]] | ||
Line 20: | Line 23: | ||
User decomposes proof into pieces, the prover checks individual steps. Typically invokes automated theorem provers and other //tactics// to show the individual steps hold. | User decomposes proof into pieces, the prover checks individual steps. Typically invokes automated theorem provers and other //tactics// to show the individual steps hold. | ||
- | Example: [[Isabelle Theorem Prover]]. | + | Example: |
+ | * [[Isabelle Theorem Prover]] | ||
+ | * [[http://pauillac.inria.fr/coq/|Coq Proof Assistant]] - popular in programming languages community | ||
+ | * [[http://www.cs.utexas.edu/~moore/acl2/|ACL2 Language and Prover]] - identifies a LISP subset with a logic | ||
+ | |||
+ | === Decision Procedure === | ||
+ | |||
+ | 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: | ||
+ | * integer linear arithmetic (no multiplication of variables, only by constants) | ||
+ | * linear arithmetic over reals | ||
+ | * formulas of first-order logic, without quantifiers | ||
+ | |||
+ | Example theories for which no decision procedure exists: | ||
+ | * arithmetic with multiplication | ||
+ | |||
+ | Semidecision procedure: must terminate if answer is "yes", need not terminate if answer is "no". | ||
+ | * Example: first-order logic | ||
+ | |||
+ | **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 === | ||
+ | |||
+ | Recall the big picture in [[Verification as Science]]. What is the role of the theorem prover? | ||
Role of prover in analysis: analyzer asks theorem prover questions | Role of prover in analysis: analyzer asks theorem prover questions |