Article (Scientific journals)
Automating Free Logic in HOL, with an Experimental Application in Category Theory
Benzmüller, Christoph; Scott, Dana
2019In Journal of Automated Reasoning
Peer Reviewed verified by ORBi
 

Files


Full Text
article.pdf
Author preprint (846.37 kB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Category Theory; Free Logic; Higher-Order Logic; Semantical Embedding; Universal Reasoning; Automated Reasoning
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Benzmüller, Christoph ;  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
External co-authors :
yes
Language :
English
Title :
Automating Free Logic in HOL, with an Experimental Application in Category Theory
Publication date :
01 January 2019
Journal title :
Journal of Automated Reasoning
ISSN :
1573-0670
Publisher :
Kluwer Academic Publishers, Netherlands
Peer reviewed :
Peer Reviewed verified by ORBi
Focus Area :
Computational Sciences
Funders :
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).
Available on ORBilu :
since 04 December 2018

Statistics


Number of views
108 (0 by Unilu)
Number of downloads
550 (0 by Unilu)

Scopus citations®
 
7
Scopus citations®
without self-citations
2
OpenCitations
 
3
WoS citations
 
5

Bibliography


Similar publications



Contact ORBilu