Skip navigation
Skip navigation
A change is coming. Click to see a sneak peek of the new Open Research Repository.

HOL Metatheory of Relevant Implication Syntax and Semantics

Download (1.08 MB)

link to publisher version

  • Altmetric Citations

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.

dc.contributor.authorTaylor, James Tanfield
dc.date.accessioned2022-07-06T02:52:36Z
dc.date.available2022-07-06T02:52:36Z
dc.identifier.urihttp://hdl.handle.net/1885/268767
dc.description.abstractWe 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.
dc.language.isoen_AU
dc.subjectRelevant Logic
dc.subjectRelevance Logic
dc.subjectNon-Classical Logic
dc.subjectRelevant Implication
dc.subjectRoutley-Meyer Semantics
dc.subjectGoldblatt Semantics
dc.subjectInteractive Theorem Proving
dc.subjectITP
dc.subjectHOL
dc.subjectHOL4
dc.subjectHigher Order Logic
dc.subjectLogic
dc.subjectMechanisation
dc.titleHOL Metatheory of Relevant Implication Syntax and Semantics
dc.typeThesis (Honours)
local.contributor.supervisorNorrish, Michael
local.contributor.supervisorcontactMichael.Norrish@anu.edu.au
dcterms.valid2022
local.description.notesDeposited by author 6.7.2022
local.type.degreeThesis (Honours)
dc.date.issued2022
local.contributor.affiliationSchool of Computing, Australian National University
local.identifier.doi10.25911/ACFH-JC17
local.mintdoimint
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
James Thesis.pdf1.08 MBAdobe PDFThumbnail
Show simple item record


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

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator