Universal Automated Theorem Prover for non-classical logics

Abstract

Non-classical logics are an adaptation of classical (boolean) logic that support nuanced forms of reasoning. This additional expressivity comes at a cost: non-classical logics tend to be more complex. This additional complexity is especially evident in the decision problem for the logic, namely when determining whether a given formula is provable in the logic. Automated theorem provers are implementations of decision procedures that can solve this problem using proof systems.

This thesis presents a generalized decision procedure for non-classical intermediate logics through an embedding into intuitionistic logic, enabled by the theory of cut-restriction that refines the standard proof system. The resulting automated theorem prover, SuperJ, is capable of proving theorems of a wide range of intermediate logics. The implementation is evaluated on a set of benchmark formulas and compared to the current state-of-the-art theorem prover intuitRIL. The results show that SuperJ is reasonably competitive with intuitRIL and could be further developed or used as a stepping stone to obtain a universal prover for non-classical logics.