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:
With Extreme Scale Computing the Rules Have Changed Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Automating Free Logic in Isabelle/HOL

verfasst von : Christoph Benzmüller, Dana Scott

Erschienen in: Mathematical Software – ICMS 2016

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present an interactive and automated theorem prover for free higher-order logic. Our implementation on top of the Isabelle/HOL framework utilizes a semantic embedding of free logic in classical higher-order logic. The capabilities of our tool are demonstrated with first experiments in category theory.

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 Towards the Automatic Discovery of Theorems in GeoGebra
Nächstes Kapitel Efficient Knot Discrimination via Quandle Coloring with SAT and #-SAT
Fußnoten
1
The numbers in https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-42432-3_6/419671_1_En_6_IEq11_HTML.gif and https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-42432-3_6/419671_1_En_6_IEq12_HTML.gif (see below) specify structural priorities and thus help to avoid brackets in formula representations.
 
2
The precise logic setting is unfortunately not discussed in the very beginning of Freyd’s and Scedrov’s textbook. Appendix B, however, contains a concise formal definition of the assumed logic. Note the special notion of equality used below (which is different from Kleene equality) and also remember that we postulated a ‘non-existing’ entity.
 
3
Metis is a trusted prover of Isabelle, since it returns proofs in Isabelle’s trusted proof kernel. Initially, however, we have worked with Isabelle’s Sledgehammer tool in our experiments, which in turn performs calls to several integrated first-order theorem provers. These calls then return valuable information on the particular proof dependencies, which in turn suggest the successful calls with metis as presented here.
 
4
By suitably adapting the Isabelle call as contained in file runIsabelle.​sh in our zip-package, the verification and generation process can be easily reproduced by the reader.
 
Literatur
1.
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J., Gabbay, D., Woods, J. (eds.) Handbook of the History of Logic, vol. 9. Logic and Computation, Elsevier (2014)
2.
3.
Freyd, P.J., Scedrov, A.: Categories, Allegories. North Holland, Amsterdam (1990)MATH
4.
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
5.
Nolt, J.: Free logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2014 edn. (2014)
6.
Scott, D.: Existence and description in formal logic. In: Schoenman, R., Russell, B. (eds.) Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967). Reprinted with additions. In: Lambert, K. (ed.) Philosophical Application of Free Logic, pp. 28–48. Oxford Universitry Press, 1991
7.
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
8.
9.
Wisniewski, M., Steen, A., Benzmüller, C.: LeoPARD — a generic platform for the implementation of higher-order reasoners. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 325–330. Springer, Heidelberg (2015)CrossRef
Metadaten
Titel
Automating Free Logic in Isabelle/HOL
verfasst von
Christoph Benzmüller
Dana Scott
Copyright-Jahr
2016
Buch
Mathematical Software – ICMS 2016

Print ISBN: 978-3-319-42431-6

Electronic ISBN: 978-3-319-42432-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-42432-3_6