Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/81425
Title: Private Names in Non-Commutative Logic
Authors: Horne, Ross
Tiu, Alwen
Aman, Bogdan
Ciobanu, Gabriel
Keywords: process calculi
calculus of structures
Issue Date: 2016
Source: Horne, R., Tiu, A., Aman, B., & Ciobanu, G. (2016). Private Names in Non-Commutative Logic. 27th International Conference on Concurrency Theory (CONCUR 2016), 31-, 1-14.
Abstract: We present an expressive but decidable first-order system (named MAV1) defined by using the calculus of structures, a generalisation of the sequent calculus. In addition to first-order universal and existential quantifiers the system incorporates a de Morgan dual pair of nominal quantifiers called `new' and `wen', distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of the operators `new' and `wen' is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as predicates in MAV1. Modelling processes as predicates in MAV1 has the advantage that linear implication defines a precongruence over processes that fully respects causality and branching. The transitivity of this precongruence is established by novel techniques for handling first-order quantifiers in the cut elimination proof.
URI: https://hdl.handle.net/10356/81425
http://hdl.handle.net/10220/41534
DOI: 10.4230/LIPIcs.CONCUR.2016.31
Rights: © 2016 The Authors (published by 27th International Conference on Concurrency Theory (CONCUR 2016)). Licensed under Creative Commons License CC-BY.
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Conference Papers

Files in This Item:
File Description SizeFormat 
p31-Horne.pdf576.44 kBAdobe PDFThumbnail
View/Open

SCOPUSTM   
Citations

3
checked on Jul 16, 2020

Page view(s)

141
checked on Sep 22, 2020

Download(s)

66
checked on Sep 22, 2020

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.