# 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

#### Interactive Provers

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.

Example:

- Coq Proof Assistant - popular in programming languages community
- 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

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