A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search

Simple item page
dc.contributor.authorHou, Zhe
dc.contributor.authorTiu, Alwen
dc.contributor.authorGore, Rajeev
dc.contributor.editorGalmiche, D.
dc.contributor.editorLarchey-Wendling, D.
dc.coverage.spatialNancy France
dc.date.accessioned2015-12-10T23:18:46Z
dc.date.createdSeptember 16-19 2013
dc.date.issued2013
dc.date.updated2019-08-11T08:17:14Z
dc.description.abstractWe present a labelled sequent calculus for Boolean BI (BBI), a classical variant of the logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in the calculus, i.e., those r
dc.identifier.isbn9783642405365
dc.identifier.urihttp://hdl.handle.net/1885/65771
dc.publisherSpringer-Verlag Berlin Heidelberg
dc.relation.ispartofseriesTABLEAUX 2013
dc.sourceTABLEAUX 2013, International Conference on Theorem Proving with Analytic Tableaux and Related Systems
dc.source.urihttp://tableaux13.loria.fr/call-papers.html
dc.subjectKeywords: Bunched implications; Concrete model; Constraint systems; Cut elimination; Logical rules; Sequent calculus; Structural rules; Ternary relations; Differentiation (calculus); Heuristic methods; Semantics; Calculations
dc.titleA Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
dc.typeConference paper
local.bibliographicCitation.lastpage187
local.bibliographicCitation.startpage172
local.contributor.affiliationHou, Zhe, College of Engineering and Computer Science, ANU
local.contributor.affiliationTiu, Alwen, College of Engineering and Computer Science, ANU
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.authoruidHou, Zhe, u4811244
local.contributor.authoruidTiu, Alwen, u4301469
local.contributor.authoruidGore, Rajeev, u9409448
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.absfor080299 - Computation Theory and Mathematics not elsewhere classified
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
local.identifier.ariespublicationu4334215xPUB1157
local.identifier.doi10.1007/978-3-642-40537-2_16
local.identifier.scopusID2-s2.0-84885731803
local.type.statusPublished Version

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
01_Hou_A_Labelled_Sequent_Calculus_2013.pdf
Size:
277.73 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS