Reference : Automating Free Logic in HOL, with an Experimental Application in Category Theory
Scientific journals : Article
Engineering, computing & technology : Computer science
Computational Sciences
http://hdl.handle.net/10993/37593
Automating Free Logic in HOL, with an Experimental Application in Category Theory
English
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]
1-Jan-2019
Journal of Automated Reasoning
Kluwer Academic Publishers
Yes
International
0168-7433
1573-0670
Netherlands
[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
http://hdl.handle.net/10993/37593
10.1007/s10817-018-09507-7
http://dx.doi.org/10.13140/RG.2.2.11432.83202

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
article.pdfAuthor preprint826.53 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.