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.