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 09:21] vkuncak |
sav08:theorem_prover [2008/02/21 09:47] 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 23: | 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 === | ||
| - | 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 39: | Line 42: | ||
| Semidecision procedure: must terminate if answer is "yes", need not terminate if answer is "no". | Semidecision procedure: must terminate if answer is "yes", need not terminate if answer is "no". | ||
| * Example: first-order logic | * 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 | ||