- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

sav07_lecture_5_skeleton [2007/03/28 17:57] vkuncak |
sav07_lecture_5_skeleton [2007/03/28 23:02] (current) 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 102: | Line 102: | ||

* 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 | + | More information: Chapter 5.4 of [[Gallier Logic Book]]. |

- | (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 | + | |