Two important techniques:

• Nelson-Oppen combination method
• Proof search

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 (n < 100) /*: inv "∀i. 0 <= i & i < n --> a[i] > 0" */ 
{
  a[n] = 1;
  n = n + 1;
}

Preservation of loop invariant: prove validity of

(∀i. 0 <= i & i < n --> a[i] > 0) -->
(∀i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0)

or satisfiability of

(∀i. 0 <= i & i < n --> a[i] > 0) & 
(∃i. 0 <= i & i < n+1 & a(n:=1)(i) <= 0)

The above formula for satisfiability can be derived using the negation of the invariant loop formula:

¬((∀i. 0 <= i & i < n --> a[i] > 0) --> (∀i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0)) <=>
(∀i. 0 <= i & i < n --> a[i] > 0) & ¬(∀i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0) <=>             ( because ¬(F1 --> F2) <=> F1 & ¬F2 )
(∀i. 0 <= i & i < n --> a[i] > 0) & (∃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: (To remove the universal quantifier, we can replace the bound variable by instantiating it with an arbitrary constant. Skolemization: Variables bound by existential quantifiers which are not inside the scope of universal quantifiers can simply be replaced by constants. In this case, we use the same constant that we used earlier to instantiate for removing the universal quantifier.)

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

The above weaker quantifier-free formula can be further simplified

(0 ⇐ i & i < n –> a(i) > 0) & (0 ⇐ i & i < n+1 & a(n:=1)(i) ⇐ 0) ⇔

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

Then as in the formula we are using two different models, we can flatten it with the purpose to use a unique theory (Linear Arithmetic). So, we define

 v = a(n:=1)(i)
 a[n |-> 1](i) <=> (v = 1 & i = n) | (v = a(i) & i ≠ n)

and we finally obtain

 (¬(0 <= i) | ¬(i <= n) | (a(i) > 0)) & ((0 <= i) & (i < n+1) & (a(n:=1)(i) <= 0))  <=>
 (¬(0 <= i) | ¬(i <= n) | (a(i) > 0)) & ((0 <= i) & (i < n+1) & (v <= 0) & (v = a(i) & i ≠ n)) <=> (distributivity)
 (¬(0 <= i) & (0 <= i) & (i < n+1) & (v <= 0) & (v = a(i) & i ≠ n)) | 
 (¬(i <= n) & (0 <= i) & (i < n+1) & (v <= 0) & (v = a(i) & i ≠ n)) | 
 ((a(i) > 0) & (0 <= i) & (i < n+1) & (v <= 0) & (v = a(i) & i ≠ n))

Note: if the formula is not satisfiable, it means that there are no counter-example and so the initial loop invariant is valid.

So we now need to find a contradiction in order to prove invariant validity. The last atom of the above formula fits well (but any other existing contradiction would have been ok)

(a(i) > 0) & (0 <= i) & (i < n+1) & (v <= 0) & (v = a(i)) & (i ≠ n) <=> (using only linear arithmetic)
(v > 0) & (0 <= i) & (i < n+1) & (v <= 0) & (i ≠ n) =>  
(v > 0) & (v <= 0) => 
⊥

The basic idea we should retain when we are dealing with multiple models is to separate formulas according to the theory (reasoning) they belong. One can use either Linear Arithmetic or the Congruence Closure algorithm. The Nelson-Oppen combination combines the two. For example, in the formula above, a(i) > 0 can be replaced by w > 0 & w = a(i). Then, we get two formulas:
(1) (w > 0) & (0 ⇐ i) & (i < n+1) & (v ⇐ 0) & (i ≠ n) &
(2) (w = a(i)) & (v = a(i))

For (2), we can use the congruence closure algorithm and obtain: v = w. This can then be used in (1), and (just by reasoning in linear arithmetic), we get a contradiction. (1) and (2) share variables and equality. Hence, we use Nelson Oppen combination with disjoint signatures. They are disjoint except for equality.

When can we merge models? If we have two formulas that are true in different models: for example: [F1]_m1 = true and [F2]_m2 = true, then what can we say about (F1 & F2) in some combination of the models? See the decomposition in the following figure:

The models can be merged if
(1)the domains are of the same size, and
(2)[x = y]_m1 –> [f(x) = f(y)]_m2, where f is an isomorphism from one model to the other.

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.

As mentioned above, The algorithm has the following steps:

1. Flatten the terms (also called separation)
2. Transform to Disjunctive Normal Form (DNF)
3. Separate Conjunctions into two groups: F1 & F2
4. Guess x_i = y_i or x_i ≠ y_i: x_i, y_i ∈ fv(F1) | fv(F2) (where fv(F) indicates free variables of F). Denote the guesses by some literals L1 & L2 & … & Ln.
5. F is satisfiable iff F1 & L1 & L2 & … & Ln is satisfiable and F2 & L1 & L2 & … & Ln is satisfiable. Each one can use different solvers.

SAT solvers could be used to avoid transforming to DNF as the latter is exponential. That is why we use the lazy approach for SAT solving as illustrated in the example below:

Example

We have the following formula:

f = ((x < y+1) | (y > z)) & ((x >= 3) | (y = 2))

To check satisfiability, we can name them: f = (p_1 | p_2) & (p_3 | p_4) where p_1 = (x < y+1), p_2 = (y > z), p_3 = (x >= 3), p_4 = (y = 2) Now, we can ask a SAT solver for a solution and the solver returns a possible assignment of truth values.

A possible assignment is: p_1 = true & p_2 = false & p_3 = true & p_4 = true The goal is, once again, to derive a contradiction.

From this assignment we obtain the following formula

(x < y+1) & ¬(y > z) & (x >= 3) & (y = 2)

And we can derive the contradiction

(x < y+1) & ¬(y > z) & (x >= 3) & (y = 2) =>
(x < y+1) & (x >= 3) & (y = 2) =>
(x < 3) & (x >= 3) => 
⊥

Then we introduce the negation of the formula that has generated the contradiction in the initial formula f. This is done so that the SAT solver doesn't return the same values again.

f' = f & ¬((x < y+1) & (x >= 3) & (y = 2)) <=>
((x < y+1) | (y > z)) & ((x >= 3) | (y = 2)) & ¬((x < y+1) & (x >= 3) & (y = 2))

Next step is rerun SAT with the improved formula f'.

• Basic idea, and in the above example (name i from the ∃i as i0, then instantiate ∀i also with i=i0)
• example:

Given: f(0) > 0 & ∀x:x > 0. (f(x)>0) –> f(x+1)>0

Prove: ∀x. (x >= 0) –> f(x+1)>0

Proof:

• f(5) > 0
  

f(5): can be derived by deriving f(1), f(2), f(3) and f(4).

• Then its straightforward to use ∀x:x > 0. (f(x)>0) –> f(x+1)>0 and arrive at the proof.

For formulas with quantifiers, example: (∀x.F1) & F2, substitute values for x in F1.

A heuristic that could be used is: Look at constants in F2 and try substituting them.

Different provers have different quantifier instantiation heuristics. See, for example, the description of the Simplify theorem prover.

To check the validity of ∀x.F1 –> ∃y.F2, y can be skolemized and we get: (∀x.F1) –> F2 If (F1[x1 := t] & ¬F2) is unsatisfiable, then ((∀x.F1) –> F2) is unsatisfiable.

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.

Recall (Tarski) semantics of first-order logic.

Can we avoid reasoning in metatheory?

Notion of formal proof.

How do we define a proof in a program?

• Set of axioms: Ax_1, Ax_2, …, Ax_n
• Set of inference rules

A proof then is nothing more than a sequence of formulas F_i.

Informal Definition: A proof is such that each F_i can be derived either from an axiom or from a rule or from a formula F_j (j < i) that we have previously derived.

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 (∀x.F) derive F[x:=t].
• generalization: after proving F which contains a fresh variable x, conclude (∀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: Paradox, Alloy tools
• Enumerating proofs gives us a way to show that formula is valid: semi decision procedure (complete but non-terminating): first-order theorem provers

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.