---
res:
bibo_abstract:
- Extensionality axioms are common when reasoning about data collections, such as
arrays and functions in program analysis, or sets in mathematics. An extensionality
axiom asserts that two collections are equal if they consist of the same elements
at the same indices. Using extensionality is often required to show that two collections
are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪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 paper 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Ashutosh
foaf_name: Gupta, Ashutosh
foaf_surname: Gupta
foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Laura
foaf_name: Kovács, Laura
foaf_surname: Kovács
- foaf_Person:
foaf_givenName: Bernhard
foaf_name: Kragl, Bernhard
foaf_surname: Kragl
foaf_workInfoHomepage: http://www.librecat.org/personId=320FC952-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0001-7745-9117
- foaf_Person:
foaf_givenName: Andrei
foaf_name: Voronkov, Andrei
foaf_surname: Voronkov
bibo_doi: 10.1007/978-3-319-11936-6_14
bibo_volume: 8837
dct_date: 2014^xs_gYear
dct_language: eng
dct_publisher: Springer@
dct_title: Extensional crisis and proving identity@
...