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]
2019
Journal of Automated Reasoning
Kluwer Academic Publishers
Yes (verified by ORBilu)
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.
Researchers ; Professionals ; Students
http://hdl.handle.net/10993/37593
http://dx.doi.org/10.13140/RG.2.2.11432.83202

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
article-20.pdfAuthor preprint907.5 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.