Mechanizing relevant logics with HOL

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 are have dealt with so far includes Routley and Meyer's R system (originally Hilbert-type axiomatization) and Read's R system (basically Gentzen-type 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 far traditional theorem provers and even relevant logicians.