Abstract
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.
Cite
CITATION STYLE
Wisniewski, M., Steen, A., Kern, K., & BenzmÜller, C. (2016). Effective normalization techniques for HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9706, pp. 362–370). Springer Verlag. https://doi.org/10.1007/978-3-319-40229-1_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
