# Lecture 5 Skeleton

Two important techniques:

- Nelson-Oppen combination method
- Proof search

## Basic idea of Nelson-Oppen combination

We mentioned decision procedures for

- quantifier-free Presburger arithmetic: by small model property
- quantifier-free uninterpreted function symbols: by congruence closure

We now show how to combine these two using Nelson-Oppen combination technique.

#### Example

n = 0; while /*: inv "ALL i. 0 <= i & i < n --> a[j] > 0" */ (n < 100) { a[n] = 1; n = n + 1; }

Preservation of loop invariant: prove validity of

(ALL i. 0 <= i & i < n --> a(j) > 0) --> (ALL i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0)

or satisfiability of

(ALL i. 0 <= i & i < n --> a(i) > 0) & (EX i. 0 <= i & i < n+1 & a(n:=1)(i) <= 0)

Let us prove a weaker quantifier-free property (by skolemizing and instantiating the quantifier):

(0 <= i & i < n --> a(i) > 0) & 0 <= i & i < n+1 & a(n:=1)(i) <= 0

Soundness in example.

Completeness by an example graph.

When can we merge models?

- the same number of nodes
- same properties on shared symbols (equality and sometimes more)

Lazy approach to integrating solvers for conjunctions and SAT solvers

### General case

In general, consider quantifier-free formulas with both linear arithmetic and uninterpreted functions.

- disjunctive normal form
- flatten
- separate
- check satisfiability separately

The harder part: proving that it is complete.

Using a SAT solver to enumerate disjunctive normal form disjuncts.

Standard for satisfiability checking of formulas, competition: http://combination.cs.uiowa.edu/smtlib

Note: we can also encode entire formula into SAT.

For more details, see Combination of Decision Procedures Summer School 2004.

### Quantifier instantiation

- Basic idea, and in the above example (name i from the EX i as i0, then instantiated ALL i also with i=i0)
- examples of incompleteness:

f(0) & ALL x. 0 <= x & f(x)>0 --> f(x+1)>0

Derive:

- f(5)
- ALL x. 0 ⇐ x –> f(x) > 0

## The notion of formal proof

Recall (Tarski) semantics of first-order logic.

Can we avoid reasoning in metatheory?

Notion of formal proof.

Minimality and independence of axioms - not so important for us.

Proof rules for first-order logic.

- propositional axioms: an instance of propositional tautology is an axiom
- instantiation: from (ALL x.F) derive F[x:=t].
- generalization: after proving F which contains a fresh variable x, conclude (ALL x.F)

Example: axiomatizing some set operations. Recall also axiomatization of equality.

We have seen two different techniques:

- Enumerating finite models (last time) gives us a way to show formula is satisfiable
- Enumerating proofs gives us a way to show that formula is valid: semi decision procedure (complete but non-terminating)

The gap in the middle: invalid formulas with only infinite models

- an example with only infinite models: strict partial order with no upper bound

Resolution theorem proving: see next lecture.

More information: Chapter 5.4 of Gallier Logic Book.