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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The numbers in
and
(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.
References
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)
Blanchette, J., Böhme, S., Paulson, L.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)
Freyd, P.J., Scedrov, A.: Categories, Allegories. North Holland, Amsterdam (1990)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nolt, J.: Free logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2014 edn. (2014)
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
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010)
Wenzel, M.: The isabelle system manual, February 2016. https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/system.pdf
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Benzmüller, C., Scott, D. (2016). Automating Free Logic in Isabelle/HOL. In: Greuel, GM., Koch, T., Paule, P., Sommese, A. (eds) Mathematical Software – ICMS 2016. ICMS 2016. Lecture Notes in Computer Science(), vol 9725. Springer, Cham. https://doi.org/10.1007/978-3-319-42432-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-42432-3_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42431-6
Online ISBN: 978-3-319-42432-3
eBook Packages: Computer ScienceComputer Science (R0)