Encoding monomorphic and polymorphic types. (English) Zbl 1445.68327
Summary: Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of “cover”. The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Software:
Why3; Metis_; Isabelle/HOL; TPTP; VAMPIRE; z3; MPTP 0.2; Jahob; Sledgehammer; E Theorem Prover; BoogieReferences:
| [1] | Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Inf. Comput. 121(2), 172–192 (1995) · Zbl 0833.68115 |
| [2] | Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II–A cooperative automatic theorem prover for higher-order logic. In: A. Armando, P. Baumgartner, G. Dowek (eds.) IJCAR 2008, LNAI, vol. 5195, pp. 162–170. Springer (2008) · Zbl 1165.68446 |
| [3] | Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reasoning 51(1), 109–128 (2013) · Zbl 1314.68272 |
| [4] | Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Empirical data associated with this article. http://www21.in.tum.de/ blanchet/enc_types_data_lmcs.tar.gz(2012) |
| [5] | Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: N. Piterman, S. Smolka (eds.) TACAS 2013, LNCS, vol. 7795, pp. 493–507. Springer (2013) · Zbl 1381.68259 |
| [6] | Blanchette, J.C., Krauss, A.: Monotonicity inference for higher-order formulas. J. Autom. Reasoning 47(4), 369–398 (2011) · Zbl 1266.03021 |
| [7] | Blanchette, J.C., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism. In: M.P. Bonacina (ed.) CADE-24, LNAI, vol. 7898, pp. 414–420. Springer (2013) · Zbl 1381.68260 |
| [8] | Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: P. Fontaine, C. Ringeissen, R.A. Schmidt (eds.) FroCoS 2013, LNCS, vol. 8152, pp. 245–260. Springer (2013) · Zbl 1398.68479 |
| [9] | Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle–Superposition with hard sorts and configurable simplification. In: L. Beringer, A. Felty (eds.) ITP 2012, LNCS, vol. 7406, pp. 345–360. Springer (2012) · Zbl 1360.68742 |
| [10] | Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: C. Barrett, L. de Moura (eds.) SMT 2008 (2008) |
| [11] | Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: K.R.M. Leino, M. Moskal (eds.) Boogie 2011, pp. 53–64 (2011) |
| [12] | Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: C. Tinelli, V. Sofronie-Stokkermans (eds.) FroCoS 2011, LNCS, vol. 6989, pp. 87–102. Springer (2011) · Zbl 1348.68215 |
| [13] | Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: J. Giesl, R. Hähnle (eds.) IJCAR 2010, LNAI, vol. 6173, pp. 107–121. Springer (2010) · Zbl 1291.68327 |
| [14] | Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in the Jahob data structure verification system. In: B. Cook, A. Podelski (eds.) VMCAI 2007, LNCS, vol. 4349, pp. 74–88. Springer (2007) · Zbl 1132.68348 |
| [15] | Claessen, K., Lillieström, A.: Automated inference of finite unsatisfiability. J. Autom. Reasoning 47(2), 111–132 (2011) · Zbl 1243.68266 |
| [16] | Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity–Translating between manysorted and unsorted first-order logic. In: N. Bjørner, V. Sofronie-Stokkermans (eds.) CADE-23, LNAI, vol. 6803, pp. 207–221. Springer (2011) · Zbl 1341.03017 |
| [17] | Couchot, J.F., Lescuyer, S.: Handling polymorphism in automated deduction. In: F. Pfenning (ed.) CADE-21, LNAI, vol. 4603, pp. 263–278. Springer (2007) · Zbl 1213.68568 |
| [18] | Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press (1972) · Zbl 0298.02002 |
| [19] | Hodges, W.: Model Theory. Cambridge University Press (1993) · Zbl 0789.03031 |
| [20] | Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: M. Archer, B. Di Vito, C. Muñoz (eds.) Design and Application of Strategies/Tactics in Higher Order Logics, no. CP-2003212448 in NASA Tech. Reports, pp. 56–68 (2003) |
| [21] | Leino, K.R.M., Rümmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: J. Esparza, R. Majumdar (eds.) TACAS 2010, LNCS, vol. 6015, pp. 312–327. Springer (2010) · Zbl 1284.68409 |
| [22] | Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008) · Zbl 1203.68188 |
| [23] | de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: C.R. Ramakrishnan, J. Rehof (eds.) TACAS 2008, LNCS, vol. 4963, pp. 337–340. Springer (2008) |
| [24] | Nipkow, T., Klein, G.: Concrete Semantics–with Isabelle/HOL. Springer (2014) |
| [25] | Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, · Zbl 0994.68131 |
| [26] | Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: K. Schneider, J. Brandt (eds.) TPHOLs 2007, LNCS, vol. 4732, pp. 232–245. Springer (2007) · Zbl 1144.68364 |
| [27] | Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm. 15(2-3), 91–110 (2002) · Zbl 1021.68082 |
| [28] | Schulz, S.: System description: E 0.81. In: D. Basin, M. Rusinowitch (eds.) IJCAR 2004, LNAI, vol. 3097, pp. 223–228. Springer (2004) · Zbl 1126.68578 |
| [29] | Stickel, M.E.: Schubert’s steamroller problem: Formulations and solutions. J. Autom. Reasoning 2(1), 89–101 (1986) · Zbl 0642.68164 |
| [30] | Sutcliffe, G.: The TPTP problem library and associated infrastructure–The FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009) · Zbl 1185.68636 |
| [31] | Sutcliffe, G.: Proceedings of the 6th IJCAR ATP system competition (CASC-J6). In: G. Sutcliffe (ed.) CASC-J6, EPiC, vol. 11, pp. 1–50. EasyChair (2012) |
| [32] | Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: N. Bjørner, A. Voronkov (eds.) LPAR-18, LNCS, vol. 7180, pp. 406–419. Springer (2012) · Zbl 1352.68217 |
| [33] | Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006) · Zbl 1113.68095 |
| [34] | Weidenbach, C.: Combining superposition, sorts and splitting. In: A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1965–2013. Elsevier (2001) · Zbl 1011.68129 |
| [35] | Wenzel, M.: Type classes and overloading in higher-order logic. In: E.L. Gunter, A. Felty (eds.) TPHOLs 1997, LNCS, vol. 1275, pp. 307–322. Springer (1997) |
| [36] | Wick, C.A., McCune, W.W.: Automated reasoning about elementary point-set topology. J. Autom. Reasoning 5(2), 239–255 (1989) 1. Introduction2. Background: Logics2.1. Polymorphic First-Order Logic2.2. Monomorphic First-Order Logic2.3. Untyped First-Order Logic2.4. Type Encodings3. Traditional Type Encodings3.1. Full Type Erasure3.2. Type Arguments3.3. Type Tags3.4. Type Guards4. Cover-Based Encodings of Polymorphism4.1. Cover-Based Type Guards4.2. Cover-Based Type Tags4.3. Polymorphic Löwenheim–Skolem5. Monotonicity-Based Type Encodings – The Monomorphic Case5.1. Monotonicity5.2. Monotonicity Inference5.3. Encoding Nonmonotonic Types5.4. Monotonicity-Based Type Tags5.5. Monotonicity-Based Type Guards5.6. Heuristic Monomorphisation6. Complete Monotonicity-Based Encodings of Polymorphism6.1. Complete Monomorphisation6.2. Monotonicity6.3. Monotonicity Inference6.4. General Strategy6.5. Monotonicity-Based Type Tags6.6. Monotonicity-Based Type Guards7. Implementation7.1. Heuristic Monomorphisation Algorithm7.2. Extension to Higher-Order Logic7.3. Infinite Types and Constructors7.4. Proof Reconstruction8. Evaluation9. Related Work10. ConclusionAcknowledgementReferences |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
