Automated theorem-proving in non-classical logics

Abstract

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.