Proof theory and proof search of biintuitionistic and tense logic

Altmetric Citations
Description
In this thesis, we consider biintuitionistic logic and tense logic, as well as the combined biintuitionistic tense logic. Each of these logics contains a pair of dual connectives, for example, Rauszer's biintuitionistic logic contains intuitionistic implication and dual intuitionistic exclusion. The interaction between these dual connectives makes it nontrivial to develop a cutfree sequent calculus for these logics. In the first part of this thesis we develop a new extended sequent...[Show more]
dc.contributor.author  Postniece, Linda  

dc.date.accessioned  20181122T00:05:49Z  
dc.date.available  20181122T00:05:49Z  
dc.date.copyright  2010  
dc.identifier.other  b2569805  
dc.identifier.uri  http://hdl.handle.net/1885/150486  
dc.description.abstract  In this thesis, we consider biintuitionistic logic and tense logic, as well as the combined biintuitionistic tense logic. Each of these logics contains a pair of dual connectives, for example, Rauszer's biintuitionistic logic contains intuitionistic implication and dual intuitionistic exclusion. The interaction between these dual connectives makes it nontrivial to develop a cutfree sequent calculus for these logics. In the first part of this thesis we develop a new extended sequent calculus for biintuitionistic logic using a framework of derivations and refutations. This is the first purely syntactic cutfree sequent calculus for biintuitionistic logic and thus solves an open problem. Our calculus is sound, semantically complete and allows terminating backward proof search, hence giving rise to a decision procedure for biintuitionistic logic. In the second part of this thesis we consider the broader problem of taming proof search in display calculi, using biintuitionistic logic and tense logic as case studies. While the generality of display calculi makes it an excellent framework for designing sequent calculi for logics where traditional sequent calculi fail, this generality also leads to a large degree of nondeterminism, which is problematic for backward proofsearch. We control this nondeterminism in two ways: 1. First, we limit the structural connectives used in the calculi and consequently, the number of display postulates. Specifically, we work with nested structures which can be viewed as a tree of traditional Gentzen's sequents, called nested sequents, which have been used previously by Kashima and, independently, by Brunnler and Strafsburger and Poggiolesi to present several modal and tense logics; 2. Second, since residuation rules are largely responsible for the difficulty in finding a proof search procedure for displaylike calculi, we show how to eliminate these residuation rules using deep inference in nested sequents; Finally, we study the combined biintuitionistic tense logic, which contains the wellknown intuitionistic modal logic as a sublogic. We give a nested sequent calculus for biintuitionistic tense logic that has cutelimination, and a derived deep inference nested sequent calculus that is complete with respect to the first calculus and where contraction and residuation rules are admissible. We also show how our calculi can capture Simpson's intuitionistic modal logic [104] and Ewald's intuitionistic tense logic.  
dc.format.extent  vii, 228 leaves.  
dc.language.iso  en_AU  
dc.rights  Author retains copyright  
dc.subject.lcc  QA9.54.P67 2010  
dc.subject.lcsh  Proof theory  
dc.subject.lcsh  Logic, Symbolic and mathematical  
dc.title  Proof theory and proof search of biintuitionistic and tense logic  
dc.type  Thesis (PhD)  
local.description.notes  Thesis (Ph.D)Australian National University,  
dc.date.issued  2010  
local.type.status  Accepted Version  
local.contributor.affiliation  Australian National University.  
local.identifier.doi  10.25911/5d5fcc3a4db33  
dc.date.updated  20181121T00:07:25Z  
dcterms.accessRights  Open Access  
local.mintdoi  mint  
Collections  Open Access Theses 
Download
File  Description  Size  Format  Image 

b25698059_Postniece_Linda.pdf  58.81 MB  Adobe PDF 
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 19 May 2020/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator