Effective normalization techniques for HOL. (English) Zbl 1475.68453
Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 362-370 (2016).
Summary: Normalization procedures are an important component of most automated theorem provers. In this work we present an adaption of advanced first-order normalization techniques for higher-order theorem proving which have been bundled in a stand-alone tool. It can be used in conjunction with any higher-order theorem prover, even though the implemented techniques are primarily targeted on resolution-based provers. We evaluated the normalization procedure on selected problems of the TPTP using multiple HO ATPs. The results show a significant performance increase, in both speed and proving capabilities, for some of the tested problem instances.
For the entire collection see [Zbl 1337.68016].
For the entire collection see [Zbl 1337.68016].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
References:
| [1] | Andrews, P.: Church’s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Stanford University, Spring (2014) |
| [2] | 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) · doi:10.1007/978-3-642-22110-1_14 |
| [3] | Benzmüller, C.: Higher-order automated theorem provers. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.) All about Proofs, Proof for All. Mathematical Logic and Foundations, pp. 171–214. College Publications, London (2015) |
| [4] | Benzmüller, C., Brown, C., Kohlhase, M.: Cut-simulation, impredicativity. Log. Methods Comput. Sci. 5(1:6), 1–21 (2009) · Zbl 1160.03004 |
| [5] | Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015) · Zbl 1356.68176 · doi:10.1007/s10817-015-9348-y |
| [6] | Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010) · Zbl 1291.68326 · doi:10.1007/978-3-642-14052-5_11 |
| [7] | Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111–117. Springer, Heidelberg (2012) · Zbl 1358.68250 · doi:10.1007/978-3-642-31365-3_11 |
| [8] | Kern, K.: Improved computation of CNF in higher-order logics. Bachelor thesis, Freie Universität Berlin (2015) |
| [9] | Niles, I., Pease, A.: Towards a standard upper ontology. In: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2–9. ACM (2001) · doi:10.1145/505168.505170 |
| [10] | Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131 |
| [11] | Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 397–411. Springer, Heidelberg (1998) · Zbl 0924.03023 · doi:10.1007/BFb0054274 |
| [12] | Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 335–367. Gulf Professional Publishing, Houston (2001) · Zbl 0992.03018 · doi:10.1016/B978-044450813-3/50008-4 |
| [13] | Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. Univers. Comput. Sci. 5(3), 73–87 (1999) · Zbl 0961.68116 |
| [14] | Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8 |
| [15] | Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010) · Zbl 1211.68371 |
| [16] | Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) Cade-13. LNCS, vol. 1104, pp. 141–145. Springer, Heidelberg (1996) · doi:10.1007/3-540-61511-3_75 |
| [17] | Wisniewski, M., Steen, A., Benzmüller, C.: The Leo-III project. In: Bolotov, A., Kerber, M. (eds.) Joint Automated Reasoning Workshop and Deduktionstreffen, p. 38 (2014) |
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.
