Two important techniques:

• Nelson-Oppen combination method
• Resolution

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.

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

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.

• 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

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

Example formula: consider case where R denotes less than relation on integers and Ev denotes that integer is even

(ALL x. EX y. R(x,y))  &
(ALL x y z. R(x,y) --> R(x, plus(x,z)))  &
(Ev(x) | Ev(plus(x,1))) -->
  (ALL x. EX y. R(x,y) & E(y))

From formulas to clauses

• negation normal form
• prenex form
• Skolemization
• conjunctive normal form

Term model and herbrand theorem.

Unification as equation solving in term algebra:

• most general unifier

Resolution and factoring proof rules.

Theorem prover competition: http://www.cs.miami.edu/~tptp/

Hanbdook of Automated Reasoning: http://www.voronkov.com/manchester/handbook-ar/index.html