School of Computing

Proof Search Issues in Some Non-Classical Logics

J. M. Howe

PhD thesis, University of St Andrews, December 1998 Available as University of St Andrews Research Report CS/99/1.

Abstract

This thesis develops techniques and ideas on proof search. Proof search is used with one of two meanings. Proof search can be thought of either as the search for a yes/no answer to a query (theorem proving), or as the search for all proofs of a formula (proof enumeration). This thesis is an investigation into issues in proof search in both these senses for some non-classical logics.

Gentzen systems are well suited for use in proof search in both senses. The rules of Gentzen sequent calculi are such that implementations can be directed by the top level syntax of sequents, unlike other logical calculi such as natural deduction. All the calculi for proof search in this thesis are Gentzen sequent calculi.

In Chapter 2, permutation of inference rules for Intuitionistic Linear Logic is studied. A focusing calculus, ILLF, in the style of Andreoli (\cite{andreoli-92}) is developed. This calculus allows only one proof in each equivalence class of proofs equivalent up to permutations of inferences. The issue here is both theorem proving and proof enumeration.

For certain logics, normal natural deductions provide a proof-theoretic semantics. Proof enumeration is then the enumeration of all these deductions. Herbelin's cut-free LJT (\cite{herb-95}, here called MJ) is a Gentzen system for intuitionistic logic allowing derivations that correspond in a 1--1 way to the normal natural deductions of intuitionistic logic. This calculus is therefore well suited to proof enumeration. Such calculi are called `permutation-free' calculi. In Chapter 3, MJ is extended to a calculus for an intuitionistic modal logic (due to Curry) called Lax Logic. We call this calculus PFLAX. The proof theory of MJ is extended to PFLAX.

Chapter 4 presents work on theorem proving for propositional logics using a history mechanism for loop-checking. This mechanism is a refinement of one developed by Heuerding \emph{et al} (\cite{heu-sey-zim-96}). It is applied to two calculi for intuitionistic logic and also to two modal logics: Lax Logic and intuitionistic S4. The calculi for intuitionistic logic are compared both theoretically and experimentally with other decision procedures for the logic.

Chapter 5 is a short investigation of embedding intuitionistic logic in Intuitionistic Linear Logic. A new embedding of intuitionistic logic in Intuitionistic Linear Logic is given. For the hereditary Harrop fragment of intuitionistic logic, this embedding induces the calculus MJ for intuitionistic logic.

In Chapter 6 a `permutation-free' calculus is given for Intuitionistic Linear Logic. Again, its proof-theoretic properties are investigated. The calculus is proved to be sound and complete with respect to a proof-theoretic semantics and (weak) cut-elimination is proved.

Logic programming can be thought of as proof enumeration in constructive logics. All the proof enumeration calculi in this thesis have been developed with logic programming in mind. We discuss at the appropriate points the relationship between the calculi developed here and logic programming.

Appendix A contains presentations of the logical calculi used and Appendix B contains the sets of benchmark formulae used in Chapter 4.

Download publication 415 kbytes

Bibtex Record

@phdthesis{946,
author = {Howe, J. M.},
title = {Proof {S}earch {I}ssues in {S}ome {N}on-{C}lassical {L}ogics},
month = {December},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Available as University of St Andrews Research Report CS/99/1},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/946},
    publication_type = {phdthesis},
    school = {University of St Andrews},
    submission_id = {22316_945702442},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014