Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Logical Framework for Developing and Mechanizing Set Theories Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Effective Normalization Techniques for HOL

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

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Internal Guidance for Satallax
Nächstes Kapitel Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition
Fußnoten
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.
 
Literatur
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.
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015)MathSciNetCrossRefMATH
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)
Metadaten
Titel
Effective Normalization Techniques for HOL
verfasst von
Max Wisniewski
Alexander Steen
Kim Kern
Christoph Benzmüller
Copyright-Jahr
2016
Buch
Automated Reasoning

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

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

Copyright-Jahr: 2016

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