Mechanizing relevant logics with HOL

Abstract

Relevant logics are non-classical logics, whose motivation is to remove logical fallacies caused by the classical “implication≓. In this paper, we propose a method to build an interactive theorem prover for relevant logics. This is done first by translating the possible world semantics for relevant logics to the higher-order representation of HOL, and then under the HOL theory obtained by this translation, relevant formulas are shown to be valid using the powerful HOL proof capabilities such as backward reasoning with tactics and tacticals. Relevant logics we have dealt with so far includes Routley and Meyer's R system (originally Hilbert-type axiomatization) and Read's R system (basically Gentzentype axiomatization). Our various proof experiences of relevant formulas by HOL and their analyses yielded a powerful proof heuristics for relevant logics. It actually allowed us to prove a formula which has been known to be difficult for traditional theorem provers and even relevant logicians.