Author(s):

Gupta, Ashutosh K; Kovács, Laura I; Kragl, Bernhard; Voronkov, Andrei V

Title: 
Extensional crisis and proving identity

Title Series: 
LNCS

Affiliation 
IST Austria 
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 firstorder theorem provers to easily solve problems no modern firstorder 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 firstorder problems that were never solved before by any prover.

Keywords: 
program analysis; theorem proving; Set theory; Problem solving; Functions; Biomineralization; Open systems; Data collection; Extensionality; First order problems; Inference rules; Superposition theorem; Theorem provers; TPTP library

Conference Title:

ATVA: Automated Technology for Verification and Analysis

Volume: 
8837

Publisher:

Springer

Date Published:

20140101

Start Page: 
185

End Page:

200

Sponsor: 
This research was supported in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), the Swedish VR grant D0497701, the Austrian National Research Network RiSE (FWF grants S11402N23 and S11410N23), and the WWTF PROSEED grant

URL: 

DOI: 
10.1007/9783319119366_14

Open access: 
yes (repository) 