Automated theorem-proving in non-classical logics
Paul B. Thistlewaite · ANU Open Research (Australian National University) · 1984
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 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.