Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_5_skeleton [2007/03/28 11:08] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 23:02] vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
Two important techniques: | Two important techniques: | ||
* Nelson-Oppen combination method | * Nelson-Oppen combination method | ||
- | * Resolution | + | * Proof search |
===== Basic idea of Nelson-Oppen combination ===== | ===== Basic idea of Nelson-Oppen combination ===== | ||
Line 25: | Line 25: | ||
Preservation of loop invariant: prove validity of | Preservation of loop invariant: prove validity of | ||
(ALL i. 0 <= i & i < n --> a(j) > 0) --> | (ALL i. 0 <= i & i < n --> a(j) > 0) --> | ||
- | (ALL i. 0 <= i & i < n+1 --> a(n:=1)(j) > 0) | + | (ALL i. 0 <= i & i < n+1 --> a(n:=1)(i) > 0) |
or satisfiability of | or satisfiability of | ||
(ALL i. 0 <= i & i < n --> a(i) > 0) & | (ALL i. 0 <= i & i < n --> a(i) > 0) & | ||
- | (EX i. 0 <= i & i < n+1 & a(n:=1)(j) >= 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): | 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 --> a(i) > 0) & | ||
- | 0 <= i & i < n+1 & a(n:=1)(i) >= 0 | + | 0 <= i & i < n+1 & a(n:=1)(i) <= 0 |
Soundness in example. | Soundness in example. | ||
Line 56: | Line 56: | ||
The harder part: proving that it is complete. | The harder part: proving that it is complete. | ||
- | |||
Using a SAT solver to enumerate disjunctive normal form disjuncts. | Using a SAT solver to enumerate disjunctive normal form disjuncts. | ||
Line 65: | Line 64: | ||
For more details, see [[http://verify.stanford.edu/summerschool2004|Combination of Decision Procedures Summer School 2004]]. | For more details, see [[http://verify.stanford.edu/summerschool2004|Combination of Decision Procedures Summer School 2004]]. | ||
- | |||
- | |||
- | |||
==== Quantifier instantiation ==== | ==== Quantifier instantiation ==== | ||
- | * Basic idea, and in the above example | + | * 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: | * examples of incompleteness: | ||
Line 79: | Line 75: | ||
* f(5) | * f(5) | ||
* ALL x. 0 <= x --> f(x) > 0 | * ALL x. 0 <= x --> f(x) > 0 | ||
- | |||
- | |||
Line 94: | Line 88: | ||
Proof rules for first-order logic. | Proof rules for first-order logic. | ||
- | * propositional axioms | + | * propositional axioms: an instance of propositional tautology is an axiom |
- | * instantiation | + | * instantiation: from (ALL x.F) derive F[x:=t]. |
- | * generalization | + | * generalization: after proving F which contains a fresh variable x, conclude (ALL x.F) |
Example: axiomatizing some set operations. | Example: axiomatizing some set operations. | ||
- | Axiomatization of equality. | + | Recall also axiomatization of equality. |
- | Two different techniques (recall we can take negation of formulas): | + | We have seen two different techniques: |
* Enumerating finite models (last time) gives us a way to show formula is satisfiable | * 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) | * 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 | The gap in the middle: invalid formulas with only infinite models | ||
* an example with only infinite models: strict partial order with no upper bound | * an example with only infinite models: strict partial order with no upper bound | ||
- | ===== Resolution theorem proving ===== | + | Resolution theorem proving: see next lecture. |
- | + | ||
- | 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 | + | More information: Chapter 5.4 of [[Gallier Logic Book]]. |