Private Names in Non-Commutative Logic
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 `...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Conference Paper |
| Language: | English |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/81425 http://hdl.handle.net/10220/41534 |
| _version_ | 1826125230445166592 |
|---|---|
| author | Horne, Ross Tiu, Alwen Aman, Bogdan Ciobanu, Gabriel |
| author2 | School of Computer Engineering |
| author_facet | School of Computer Engineering Horne, Ross Tiu, Alwen Aman, Bogdan Ciobanu, Gabriel |
| author_sort | Horne, Ross |
| collection | NTU |
| description | 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. |
| first_indexed | 2024-10-01T06:33:18Z |
| format | Conference Paper |
| id | ntu-10356/81425 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T06:33:18Z |
| publishDate | 2016 |
| record_format | dspace |
| spelling | ntu-10356/814252020-05-28T07:18:32Z Private Names in Non-Commutative Logic Horne, Ross Tiu, Alwen Aman, Bogdan Ciobanu, Gabriel School of Computer Engineering 27th International Conference on Concurrency Theory (CONCUR 2016) process calculi calculus of structures 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. MOE (Min. of Education, S’pore) Published version 2016-10-03T07:57:04Z 2019-12-06T14:30:41Z 2016-10-03T07:57:04Z 2019-12-06T14:30:41Z 2016 Conference Paper 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. https://hdl.handle.net/10356/81425 http://hdl.handle.net/10220/41534 10.4230/LIPIcs.CONCUR.2016.31 en © 2016 The Authors (published by 27th International Conference on Concurrency Theory (CONCUR 2016)). Licensed under Creative Commons License CC-BY. 14 p. application/pdf |
| spellingShingle | process calculi calculus of structures Horne, Ross Tiu, Alwen Aman, Bogdan Ciobanu, Gabriel Private Names in Non-Commutative Logic |
| title | Private Names in Non-Commutative Logic |
| title_full | Private Names in Non-Commutative Logic |
| title_fullStr | Private Names in Non-Commutative Logic |
| title_full_unstemmed | Private Names in Non-Commutative Logic |
| title_short | Private Names in Non-Commutative Logic |
| title_sort | private names in non commutative logic |
| topic | process calculi calculus of structures |
| url | https://hdl.handle.net/10356/81425 http://hdl.handle.net/10220/41534 |
| work_keys_str_mv | AT horneross privatenamesinnoncommutativelogic AT tiualwen privatenamesinnoncommutativelogic AT amanbogdan privatenamesinnoncommutativelogic AT ciobanugabriel privatenamesinnoncommutativelogic |