Title:Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic

Tags:Automated Theorem Proving, Axiomatic Category Theory, Free Logic, Higher-Order Logic, Model Finding, SMT and SAT and Universal Logical Reasoning

Abstract:

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a universal logical reasoning engine. Such an engine may be employed, as already envisioned by Leibniz, to support the rigorous formalisation and deep logical analysis of rational arguments on the computer.

In my talk I will exemplarily demonstrate how this approach can be utilised to implement "free logic" within the proof assistant Isabelle/HOL. SMT solvers and ATPs, which are integrated with Isabelle/HOL, can be then be used in this framework to (indirectly) automate free logic reasoning.

Free logic has many interesting applications, e.g. in natural language processing and as a logic of fiction. In mathematics, free logics are particularly suited in application domains, such as axiomatic category theory, where an adequate and elegant treatment of partiality and undefinedness is required.

In my talk I will summarise the results of an experiment with the above free logic reasoner, in which a series of mutually equivalent axiom systems for category theory has been systematically explored. As a side-effect of this work some (minor) issue in a prominent category theory textbook has been revealed.

The purpose of this work is not to claim any novel results in category theory, but to demonstrate an elegant way to automate reasoning in free logic, and to present illustrative experiments, which were (indirectly) supported by SMT solvers, ATPs and the model finder Nitpick.

Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic

Invited talk: Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic