Extensional crisis and proving identity Conference Paper


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 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.
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: 2014-01-01
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 S11402-N23 and S11410-N23), and the WWTF PROSEED grant
URL:
DOI: 10.1007/978-3-319-11936-6_14
Open access: yes (repository)
IST Austria Authors
  1. Ashutosh Gupta
    16 Gupta
  2. Bernhard Kragl
    5 Kragl
Related IST Austria Work