Search

• < Previous
• 1
• Next >

---

A System of Interaction and Structure II: The Need for Deep Inference

Alwen Tiu.

This paper studies properties of the logic BV, which is an extension of multiplicative linear logic (MLL) with a self-dual non-commutative operator. BV is presented in the calculus of structures, a proof theoretic formalism that supports deep inference, in which inference rules can be applied&nbsp;[&hellip;]

---

A Proof Theoretic Analysis of Intruder Theories

Alwen F Tiu ; Rajeev Gore ; Jeremy Dawson.

We consider the problem of intruder deduction in security protocol analysis: that is, deciding whether a given message M can be deduced from a set of messages Gamma under the theory of blind signatures and arbitrary convergent equational theories modulo associativity and commutativity (AC) of&nbsp;[&hellip;]

---

On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics

Rajeev Gore ; Linda Postniece ; Alwen F Tiu.

We consider two styles of proof calculi for a family of tense logics, presented in a formalism based on nested sequents. A nested sequent can be seen as a tree of traditional single-sided sequents. Our first style of calculi is what we call "shallow calculi", where inference rules are only applied&nbsp;[&hellip;]

---

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

Ki Yung Ahn ; Ross Horne ; Alwen Tiu.

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are&nbsp;[&hellip;]

---