|
Abstract : |
We introduce the logic of bunched implications, BI, in which multiplicative (or linear) and additive (or intuitionistic) implications live side-by-side. We provide a truth conditional semantics, a proof theory and a categorical semantics of proofs. We explain how BI arises as a logic of resources and sketch a development of this computational interpretation, which is quite different from that of linear logic, in the setting of logic programming. Predicate BI, used in our account of logic programming, admits not only the usual (additive) quantifiers but also multiplicative (or intensional) quantifiers if the kind long sought in relevant logic. 1, |
