{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:21:52Z","timestamp":1758979312777,"version":"3.41.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T00:00:00Z","timestamp":1563235200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Ministry of Education, Singapore, Tier 2","award":["MOE2014-T2-2-076"],"award-info":[{"award-number":["MOE2014-T2-2-076"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>\n            This article explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a De Morgan dual pair of nominal quantifiers. These nominal quantifiers called \u201cnew\u201d and \u201cwen\u201d are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that \u201cnew\u201d distributes over positive operators while \u201cwen\u201d distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called\n            <jats:italic>splitting<\/jats:italic>\n            . The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction, and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.\n          <\/jats:p>","DOI":"10.1145\/3325821","type":"journal-article","created":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T12:39:01Z","timestamp":1563280741000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0162-1901","authenticated-orcid":false,"given":"Ross","family":"Horne","sequence":"first","affiliation":[{"name":"Computer Science and Communications, University of Luxembourg, Esch-sur-Alzette, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"Research School of Computer Science, The Australian National University, Canberra, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bogdan","family":"Aman","sequence":"additional","affiliation":[{"name":"Alexandru Ioan Cuza University of Ia\u015fi, Ia\u015fi, Romania"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Ciobanu","sequence":"additional","affiliation":[{"name":"Alexandru Ioan Cuza University of Ia\u015fi, Ia\u015fi, Romania"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,16]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.06.019"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-010-9241-0"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1168352668"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_24"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/645522.656476"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462186"},{"volume-title":"Quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. Logical Meth. Comput. Sci. 12, 2:5","year":"2016","author":"Bruscoli Paola","key":"e_1_2_2_10_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the EACSL Conference on Computer Science Logic","volume":"12","author":"Chaudhuri Kaustuv","year":"2011"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the International Andrei Ershov Memorial Conference (PSI\u201915)","volume":"9609","author":"Ciobanu Gabriel","year":"2015"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"e_1_2_2_15_1","unstructured":"Murdoch J. Gabbay. 2016. Consistency of Quine\u2019s New Foundations using nominal techniques. (2016). Retrieved from: arXiv:1406.4060v4.  Murdoch J. Gabbay. 2016. Consistency of Quine\u2019s New Foundations using nominal techniques. (2016). Retrieved from: arXiv:1406.4060v4."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603160"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1182613.1182614"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012951100003X"},{"key":"e_1_2_2_23_1","first-page":"245","article-title":"The consistency and complexity of multiplicative additive system virtual. Sci","volume":"25","author":"Horne Ross","year":"2015","journal-title":"Ann. Comp. Sci."},{"key":"e_1_2_2_24_1","volume-title":"Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD\u201919)","volume":"131","author":"Horne Ross","year":"2019"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1531"},{"key":"e_1_2_2_26_1","unstructured":"Ross Horne and Alwen Tiu. 2019. Constructing weak simulations from linear implications for processes with private names. Math. Struct. Comput. Sci. n.d. (2019) 1--34.  Ross Horne and Alwen Tiu. 2019. Constructing weak simulations from linear implications for processes with private names. Math. Struct. Comput. Sci. n.d. (2019) 1--34."},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 27th International Conference on Concurrency Theory (CONCUR\u201916), Leibniz International Proceedings in Informatics (LIPIcs), Jos\u00e9e Desharnais and Radha Jagadeesan (Eds.)","volume":"59","author":"Horne Ross","year":"2016"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.11.005"},{"volume-title":"Interaction and depth against nondeterminism in proof search. Logical Meth. Comput. Sci. 10, 2","year":"2014","author":"Kahramano\u011fullar\u0131 Ozan","key":"e_1_2_2_29_1"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90085-X"},{"volume-title":"Proceedings of the International Logic Programming Symposium (ILPS\u201993)","year":"1993","author":"Kobayashi Naoki","key":"e_1_2_2_31_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275674"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00107-3"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788767"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316061"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024922.1024925"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"volume-title":"A Calculus of Communicating Systems","author":"Milner Robin","key":"e_1_2_2_39_1"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Robin Milner. 1993. The polyadic &pi;-calculus: A tutorial. In Logic and Algebra of Specification Friedrich Bauer Wilfried Brauer and Helmut Schwichtenberg (Eds.). 203--246.  Robin Milner. 1993. The polyadic &pi;-calculus: A tutorial. In Logic and Algebra of Specification Friedrich Bauer Wilfried Brauer and Helmut Schwichtenberg (Eds.). 203--246.","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01379149"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645893.671608"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu033"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/645711.664616"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80853-3"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_23"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.02.022"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1970398.1970399"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(2:4)2006"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173544"},{"key":"e_1_2_2_55_1","volume-title":"Proceedings of the Conference for Computer Science Logic (CSL\u201917)","volume":"82","author":"Tubella Andrea Aler","year":"2017"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3325821","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3325821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:08Z","timestamp":1750204388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3325821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,16]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3325821"],"URL":"https:\/\/doi.org\/10.1145\/3325821","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,7,16]]},"assertion":[{"value":"2017-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}