Speaker: |
Ashutosh Gupta (Institute of Science and Technology Am campus 1 3400 Klosterneuburg Austria) |

Organiser: |
Paritosh K Pandya |

Date: |
Monday, 26 May 2014, 16:00 to 17:00 |

Venue: |
D-405 (D-Block Seminar Room) |

(Scan to add to calendar)

Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem \forall x)(\forall y) x \union y = y \union x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use.

In this work we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover.