01.01.2019 | Ausgabe 1/2020
Automating Free Logic in HOL, with an Experimental Application in Category Theory
- Zeitschrift:
- Journal of Automated Reasoning > Ausgabe 1/2020
Wichtige Hinweise
Electronic supplementary material
The online version of this article (https://doi.org/10.1007/s10817-018-09507-7) contains supplementary material, which is available to authorized users.
Benzmüller received funding from the German National Research Foundation DFG under Heisenberg grant Towards Computational Metaphysics (BE 2501/9-2) and from VolkswagenStiftung under grant Consistent Rational Argumentation in Politics (CRAP).
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Abstract
A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the formalisation and verification of free logic theories. Subsequently, this approach is applied to a selected domain of mathematics: starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. As a side-effect of this work some (minor) issues in a prominent category theory textbook have been revealed. The purpose of this article is not to claim any novel results in category theory, but to demonstrate an elegant way to “implement” and utilize interactive and automated reasoning in free logic, and to present illustrative experiments.
