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: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). (pp. 87 - 103).

Full text not available from this repository.

Abstract

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
UCL classification:UCL > School of BEAMS > Faculty of Engineering Science > Computer Science

Archive Staff Only: edit this record