This is an old revision of the document!
Lecture 5 Skeleton
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)(j) > 0)
or satisfiability of
(ALL i. 0 <= i & i < n --> a(i) > 0) & (EX i. 0 <= i & i < n+1 & a(n:=1)(j) >= 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)
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
- 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
- instantiation
- generalization
Example: axiomatizing some set operations. Axiomatization of equality.
Two different techniques (recall we can take negation of formulas):
- 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
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