In this paper, we study proof-search in the propositional BI logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. With its underlying sharing interpretation, BI has been recently used for logic programming or reasoning about mutable data structures. We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that, from a given formula A , a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we show the finite model property for BI with respect to this semantics.
We present a modal logic for describing the spatial organization and the behavior of distributed systems. In addition to standard logical and temporal operators, our logic includes spatial operations corresponding to process composition and name hiding, and a fresh quantifier.
λ Sym PA is a natural deduction system for Peano Arithmetic that was developed in order to provide a basis for the programming with-proofs paradigm in a classical logic setting. In the paper we analyze one of its main features: non-confluence. After looking at which rules can cause non-confluence, we develop in the system a formal proof for a formula that can be seen as a simple but meaningful program specification. The computational behaviour of the corresponding term will be analysed by interpreting it as a (higher-order communicating) process formed by distinct subprocesses which co-operate in different ways, producing different results, according to the reduction strategy used. We also show how to restrict the system in order to get confluence without loosing its computational features. The restricted system enables us to argue for the expressive power of symmetric and non-deterministic calculi like λ Sym PA .
