Springe direkt zu Inhalt

Automating Free Logic in HOL, with an Experimental Application in Category Theory

Christoph Benzmüller, Dana Scott – 2019

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.

Titel
Automating Free Logic in HOL, with an Experimental Application in Category Theory
Verfasser
Verlag
Kluwer Academic Publishers
Schlagwörter
Category Theory ; Free Logic ; Higher-Order Logic ; Semantical Embedding ; Universal Reasoning ; Automated Reasoning
Datum
2019-01
Kennung
ISSN : 0168-7433; e-ISSN : 1573-0670
Erschienen in
Journal of Automated Reasoning