Skip navigation
Skip navigation

Automated theorem-proving in non-classical logics

Thistlewaite, Paul Brian

Description

The topic of this dissertation lies in the intersection of logic and computer science, and rests firmly in that area of artificial intelligence (AI) known as automated theorem-proving (ATP). Our principal concern is with the design and implementation of theorem-proving programs for a range of non-classical logics, and especially for relevant family of non-classical logics detailed in [Anderson and Belnap 75]. In Chapter 1 we discuss the history of and motivations for non-classical...[Show more]

dc.contributor.authorThistlewaite, Paul Brian
dc.date.accessioned2017-12-11T23:55:08Z
dc.date.available2017-12-11T23:55:08Z
dc.date.copyright1984
dc.identifier.otherb1290070
dc.identifier.urihttp://hdl.handle.net/1885/137627
dc.description.abstractThe topic of this dissertation lies in the intersection of logic and computer science, and rests firmly in that area of artificial intelligence (AI) known as automated theorem-proving (ATP). Our principal concern is with the design and implementation of theorem-proving programs for a range of non-classical logics, and especially for relevant family of non-classical logics detailed in [Anderson and Belnap 75]. In Chapter 1 we discuss the history of and motivations for non-classical theoremproving, concentrating on the uses within logic and AI or ATP systems based on relevant logic. In Chapters 2, 3 and 4 we develop automated theorem-proving techniques for relevant logic culminating in the program KRIPKE for deciding theoremhood in the relevant logic LR. Chapter 2 is concerned with replacing the proof-theoretical formulation of LR due to Kripke and Meyer with one more attuned to the requirements of automation. ChapterĀ·3 advances the fundamentals of using algebraic models of a logic to prune the often immense search spaces generated during automated theorem proving in relevant logics. This technique is generalizable to theorem-proving in any logic that has an algebraic semantics. In Chapter 4 we discuss some of the strategic and extralogical considerations involved in making KRIPKE a viable ATP system.
dc.format.extent186 leaves
dc.language.isoen
dc.subject.lcshAutomatic theorem proving
dc.subject.lcshNonclassical mathematical logic
dc.titleAutomated theorem-proving in non-classical logics
dc.typeThesis (PhD)
local.contributor.supervisorMeyer, R. K.
local.contributor.supervisorMcRobbie, M. A.
dcterms.valid1984
local.description.notesThesis (Ph.D.)--Australian National University, 1984. This thesis has been made available through exception 200AB to the Copyright Act.
local.type.degreeDoctor of Philosophy (PhD)
dc.date.issued1984
local.contributor.affiliationThe Australian National University
local.identifier.doi10.25911/5d6fa29251193
dc.date.updated2017-11-22T22:35:06Z
local.identifier.proquestYes
local.mintdoimint
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
b12900709_Thistlewaite, Paul Brian.pdf96.41 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