Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
A Logical Framework for Developing and Mechanizing Set Theories Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Effective Normalization Techniques for HOL

Authors : Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller

Published in: Automated Reasoning

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Internal Guidance for Satallax
next chapter Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition
Footnotes
1
With #CNF we denote the number of clauses generated by transforming the given formula into clause normal form.
 
2
A comprehensive presentation of the different TPTP problem domains and their application domain can be found at http://​www.​cs.​miami.​edu/​~tptp/​cgi-bin/​SeeTPTP?​Category=​Documents&​File=​OverallSynopsis.
 
3
The average time results for normalization procedure \(N_3\) are in nearly all cases within a range of \(0.1\,\%\) of the results for \(N_1\). Likewise results apply for \(N_4\) and \(N_2\).
 
4
The prover LEO-II, for example, is able to detect such (sub-)formulas and to replace them by primitive equalities \(a = b\).
 
5
The Leonora repository can be found at https://​github.​com/​Ryugoron/​Leonora.
 
Literature
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)CrossRef
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)MathSciNetMATH
5.
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)CrossRef
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)CrossRef
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)
10.
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
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)CrossRef
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)CrossRef
13.
Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. Univers. Comput. Sci. 5(3), 73–87 (1999)MathSciNetMATH
14.
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefMATH
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)MathSciNetMATH
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)CrossRef
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)
Metadata
Title
Effective Normalization Techniques for HOL
Authors
Max Wisniewski
Alexander Steen
Kim Kern
Christoph Benzmüller
Copyright Year
2016
Book
Automated Reasoning

Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-40229-1_25

Premium Partner

    Image Credits