Reference : Automating Free Logic in HOL, with an Experimental Application in Category Theory
Scientific journals : Article
Engineering, computing & technology : Computer science
Computational Sciences
Automating Free Logic in HOL, with an Experimental Application in Category Theory
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Scott, Dana [Berkeley University of California - UC Berkeley]
Journal of Automated Reasoning
Kluwer Academic Publishers
[en] Category Theory ; Free Logic ; Higher-Order Logic ; Semantical Embedding ; Universal Reasoning ; Automated Reasoning
[en] 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 andverification of free logic theories. Subsequently, this approach is applied to aselected domain of mathematics: starting from a generalization of the standardaxioms for a monoid we present a stepwise development of various, mutuallyequivalent foundational axiom systems for category theory. As a side-effect ofthis work some (minor) issues in a prominent category theory textbook havebeen revealed.The purpose of this article is not to claim any novel results in category the-ory, but to demonstrate an elegant way to “implement” and utilize interactiveand automated reasoning in free logic, and to present illustrative experiments.
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).
Researchers ; Professionals ; Students

File(s) associated to this reference

Fulltext file(s):

Open access
article.pdfAuthor preprint826.53 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.