| Title: | Reasoning in First-Order Theories with Extensionality |
| Authors: | Ashutosh Gupta, Laura Kovacs, Bernhard Kragl and Andrei Voronkov |
| Proceedings: | Vampire 2014 Proceedings |
| Editors: | Laura Kovacs and Andrei Voronkov |
| Keywords: | first-order theorem proving, extensionality axiom, superposition calculus, saturation algorithm |
| Abstract: | Extensionality resolution is a new inference rule that helps first-order theorem provers to overcome limitations when reasoning with extensionality axioms. The inference rule naturally resembles the use of extensionality axioms in human proofs and integrates easily into the architecture of superposition-based theorem provers. The recent implementation of extensionality resolution in Vampire provides strong experimental evidence of the effectiveness of the technique. We present ongoing work on new options to control the recognition of extensionality axioms as well as the application of extensionality resolution inferences in the proof search of Vampire. |
| Pages: | 1 |
| Talk: | Jul 23 17:30 |
| Paper: |  |