Howe, Jacob M. (1998) Proof Search Issues in Some NonClassical Logics. Doctor of Philosophy (PhD) thesis, University of St Andrews. (KAR id:21574)
Other (zip)
Language: English 

Download (425kB)


PDF
Language: English 

Download (919kB)
Preview


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 nonclassical 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 (citeandreoli92) 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 prooftheoretic semantics. Proof enumeration is then the enumeration of all these deductions. Herbelin's cutfree LJT (citeherb95, here called MJ) is a Gentzen system for intuitionistic logic allowing derivations that correspond in a 11 way to the normal natural deductions of intuitionistic logic. This calculus is therefore well suited to proof enumeration. Such calculi are called `permutationfree' 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 loopchecking. This mechanism is a refinement of one developed by Heuerding emphet al (citeheuseyzim96). 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 `permutationfree' calculus is given for Intuitionistic Linear Logic. Again, its prooftheoretic properties are investigated. The calculus is proved to be sound and complete with respect to a prooftheoretic semantics and (weak) cutelimination 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.
Item Type:  Thesis (Doctor of Philosophy (PhD)) 

Additional information:  Available as University of St Andrews Research Report CS/99/1 
Subjects:  Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, 
Divisions:  Faculties > Sciences > School of Computing 
Depositing User:  Mark Wheadon 
Date Deposited:  26 Aug 2009 18:14 UTC 
Last Modified:  28 May 2019 14:01 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21574 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):