UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Formalised inductive reasoning in the logic of bunched implications

Brotherston, J; (2007) Formalised inductive reasoning in the logic of bunched implications. In: (pp. pp. 87-103).

Full text not available from this repository.


We present a framework for inductive definitions in the logic of bunched implications, BI, and formulate two sequent calculus proof systems for inductive reasoning in this framework. The first proof system adopts a traditional approach to inductive proof, extending the usual sequent calculus for predicate BI with explicit induction rules for the inductively defined predicates. The second system allows an alternative mode of reasoning with inductive definitions by cyclic proof. In this system, the induction rules are replaced by simple case-split rules, and the proof structures are cyclic graphs formed by identifying some sequent occurrences in a derivation tree. Because such proof structures are not sound in general, we demand that cyclic proofs must additionally satisfy a global trace condition that ensures soundness. We illustrate our inductive definition framework and proof systems with simple examples which indicate that, in our setting, cyclic proof may enjoy certain advantages over the traditional induction approach. © Springer-Verlag Berlin Heidelberg 2007.

Type: Proceedings paper
Title: Formalised inductive reasoning in the logic of bunched implications
ISBN-13: 9783540740605
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1353137
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item