References of "Journal of Automated Reasoning"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailAutomating Free Logic in HOL, with an Experimental Application in Category Theory
Benzmüller, Christoph UL; Scott, Dana

in Journal of Automated Reasoning (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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 79 (1 UL)