Show simple item record

dc.contributor.advisorBundy, Alanen
dc.contributor.authorWallen, Lincoln A.en
dc.date.accessioned2013-04-02T14:56:28Z
dc.date.available2013-04-02T14:56:28Z
dc.date.issued1987
dc.identifier.urihttp://hdl.handle.net/1842/6600
dc.description.abstractIn this thesis we develop efficient methods for automated proof search within an important class of mathematical logics. The logics considered are the varying, cumulative and constant domain versions of the first-order modal logics K, K4, D, D4, T, S4 and S5, and first-order intuitionistic logic. The use of these non-classical logics is commonplace within Computing Science and Artificial Intelligence in applications in which efficient machine assisted proof search is essential. Traditional techniques for the design of efficient proof methods for classical logic prove to be of limited use in this context due to their dependence on properties of classical logic not shared by most of the logics under consideration. One major contribution of this thesis is to reformulate and abstract some of these classical techniques to facilitate their application to a wider class of mathematical logics. We begin with Bibel's Connection Calculus: a matrix proof method for classical logic comparable in efficiency with most machine orientated proof methods for that logic. We reformulate this method to support its decomposition into a collection of individual techniques for improving the efficiency of proof search within a standard cut-free sequent calculus for classical logic. Each technique is presented as a means of alleviating a particular form of redundancy manifest within sequent-based proof search. One important result that arises from this anaylsis is an appreciation of the role of unification as a tool for removing certain proof-theoretic complexities of specific sequent rules; in the case of classical logic: the interaction of the quantifier rules. All of the non-classical logics under consideration admit complete sequent calculi. We anaylse the search spaces induced by these sequent proof systems and apply the techniques identified previously to remove specific redundancies found therein. Significantly, our proof-theoretic analysis of the role of unification renders it useful even within the propositional fragments of modal and intuitionistic logic.en
dc.contributor.sponsorScience and Engineering Research Councilen
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionGenerating connection calculi from tableau- and sequent-based proof systems. In A.G. Cohn and J.R. Thomas, editors, Artificial Intelligence and its Applications, pages 35-50, John Wiley & Sons, 1986. Proceedings of AISB85, Warwick, England, April 1985.en
dc.relation.hasversionFormulating proof systems for automated deduction. In Proceedings of the IEE Colloquium on Theorem Provers in Theory and Practice, March 1987.en
dc.relation.hasversionA computationally efficient proof system for S5 modal logic (with G.V. Wilson). In J. Hallam and C. Mellish, editors, Advances in Artificial Intelligence, pages 141-153, John Wiley & Sons, 1987. Proceedings of AISB87, Edinburgh, Scotland, April 1987.en
dc.relation.hasversionMatrix proof methods for modal logics. In J. McDermott, editor, Proceedings of the 10th International Joint Conference on Artificial Intelligence, pages 917-923, Morgan Kaufmann Inc., 1987.en
dc.subjectAutomatic theorem provingen
dc.subjectmathematical logicsen
dc.subjectintuitionistic logic.en
dc.subjectmatrix proof methodsen
dc.titleAutomated proof search in non-classical logics : efficient matrix proof methods for modal and intuitionistic logicsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record