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:
With Extreme Scale Computing the Rules Have Changed Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Automating Free Logic in Isabelle/HOL

Authors : Christoph Benzmüller, Dana Scott

Published in: Mathematical Software – ICMS 2016

Publisher: Springer International Publishing

Log in

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

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.

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 Towards the Automatic Discovery of Theorems in GeoGebra
next chapter Efficient Knot Discrimination via Quandle Coloring with SAT and #-SAT
Footnotes
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.
 
Literature
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
Metadata
Title
Automating Free Logic in Isabelle/HOL
Authors
Christoph Benzmüller
Dana Scott
Copyright Year
2016
Book
Mathematical Software – ICMS 2016

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

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

Copyright Year: 2016

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

Premium Partner

    Image Credits