Taylor, James Tanfield2022-07-062022-07-06http://hdl.handle.net/1885/268767We mechanise two Hilbert systems, a Natural Deduction system, the Routley-Meyer semantics, and the Cover semantics for the Relevant Logic R in HOL4. We also show equivalence results between one of the Hilbert Systems and the other Hilbert system and the Natural Deduction system. We also show soundness and completeness results between the one of the Hilbert Systems and the two Semantic systems, thereby producing machine checked proofs of all of these results.en-AURelevant LogicRelevance LogicNon-Classical LogicRelevant ImplicationRoutley-Meyer SemanticsGoldblatt SemanticsInteractive Theorem ProvingITPHOLHOL4Higher Order LogicLogicMechanisation202210.25911/ACFH-JC17