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.
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 ICT C-050.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Experimental results of this paper, http://vprover.org/extres
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New Results on Rewrite-Based Satisfiability Procedures. ACM Trans. Comput. Log. 10(1) (2009)
Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, pp. 19–99. Elsevier and MIT Press (2001)
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational Theorem Proving for Hierarchic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)
Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010), www.SMT-LIB.org
Baumgartner, P., Waldmann, U.: Hierarchic Superposition with Weak Abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 39–57. Springer, Heidelberg (2013)
Bledsoe, W.W., Boyer, R.S.: Computer Proofs of Limit Theorems. In: Proc. of IJCAI, pp. 586–600 (1971)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
de Moura, L., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45–52. IEEE (2009)
Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497–511. Springer, Heidelberg (2006)
Habermehl, P., Iosif, R., Vojnar, T.: What Else Is Decidable about Integer Arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008)
Korovin, K.: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Kovács, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013)
Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 7, pp. 371–443. Elsevier Science (2001)
Prevosto, V., Waldmann, U.: SPASS+T. In: Proc. of ESCoR, pp. 18–33 (2006)
Riazanov, A., Voronkov, A.: Limited Resource Strategy in Resolution Theorem Proving. J. of Symbolic Computation 36(1-2), 101–115 (2003)
Rümmer, P.: E-Matching with Free Variables. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 359–374. Springer, Heidelberg (2012)
Schulz, S.: System Description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009)
Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications 19(1), 35–48 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Gupta, A., Kovács, L., Kragl, B., Voronkov, A. (2014). Extensional Crisis and Proving Identity. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)