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
Yes (verified by ORBilu)
[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.
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.