Notion of Theorem Prover and Its Role in SAV
Notion of Automated Theorem Prover
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: “No, formula is not valid, here is a counterexample which shows it is false”
- TP says: “I don't know. Too hard for me (within given time/memory)”
- TP loops forever
Example automated theorem provers:
- SPASS from the Max Planck Institut for Computer Science
Combine user insight with automated techniques.
User decomposes proof into pieces, the prover checks individual steps. Typically invokes automated theorem provers and other tactics to show the individual steps hold.
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
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
- with complex enough logic, entire program correctness becomes a theorem
- program semantics tells us how this theorem looks like (we will see)
- usually this theorem is very large and difficult, so not feasible to do automatically (but can use interactive provers)
- program analyzers are specialized theorem provers - using knowledge of program structure to gain automation
- if user provides (loop) invariants, the problem reduces to multiple simple theorems
- you will build in class systems that implement this reduction
- modern analyzers can internally call prover(s) many times to synthesize invariants and check that program satisfies desired property
- you learn about examples of such systems