Lab for Automated Reasoning and Analysis LARA

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.

 
sav07_lecture_5_skeleton.txt · Last modified: 2007/03/28 23:02 by vkuncak