LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
Next revision Both sides next revision
sav07_lecture_4_skeleton [2007/03/22 18:21]
vkuncak 		sav07_lecture_4_skeleton [2007/03/22 20:30]
vkuncak
Line 8: Line 8:
  
 We use weakest preconditions,​ although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. We use weakest preconditions,​ although you could also use strongest postconditions or any other variants of the conversion from programs to formulas.
- 
- 
- 
- 
- 
  
 ===== More on wp ===== ===== More on wp =====
Line 101: Line 96:
  
 Again, the second part!  More technical. ​ But, often you can use these things as a black box. Again, the second part!  More technical. ​ But, often you can use these things as a black box.
 +
  
 ==== Congruence closure algorithm ==== ==== Congruence closure algorithm ====
Line 110: Line 106:
 Equality is a congruence with respect to all function symbols. Equality is a congruence with respect to all function symbols.
  
- +More information on congruence closure algorithm: 
-==== Basic idea of Nelson-Oppen combination ==== +  * [[Gallier Logic Book]], Chapter 10.6 
- +  * {{nelsonoppen80decisionprocedurescongruenceclosure.pdf|the original paper by Nelson ​and Oppen}}
-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. +
- +
- +
-==== Quantified formulas ==== +
- +
-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. +
- +
-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 +
-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 ==== +
- +
-From formulas to clauses +
-  * negation normal form +
-  * prenex form +
-  * Skolemization +
-  * conjunctive normal form +
- +
-Unification. +
- +
-Resolution ​and factoring proof rules. +
- +
-Theorem prover competition:​ http://​www.cs.miami.edu/​~tptp/​ +
- +
-==== Essentially propositional formulas ==== +