Skip navigation
Skip navigation

HOL Metatheory of Relevant Implication Syntax and Semantics

Taylor, James Tanfield

Description

We 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.

CollectionsOpen Access Theses
Date published: 2022
Type: Thesis (Honours)
URI: http://hdl.handle.net/1885/268767
DOI: 10.25911/ACFH-JC17

Download

File Description SizeFormat Image
James Thesis.pdf1.08 MBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator