Please use this identifier to cite or link to this item:
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.
Conference: 27th International Conference on Concurrency Theory (CONCUR 2016)
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.
DOI: 10.4230/LIPIcs.CONCUR.2016.31
Schools: School of Computer Engineering 
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

Citations 50

Updated on Jan 26, 2024

Page view(s)

Updated on Feb 21, 2024

Download(s) 50

Updated on Feb 21, 2024

Google ScholarTM




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