{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:43:19Z","timestamp":1770277399228,"version":"3.49.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003759","name":"Universidad Polit\u00e9cnica de Madrid","doi-asserted-by":"publisher","award":["RYC-2006-002131"],"award-info":[{"award-number":["RYC-2006-002131"]}],"id":[{"id":"10.13039\/501100003759","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments.<\/jats:p>\n          <jats:p>This allows for direct axiomatizations with binders, such as of the \u03bb-binder of the lambda-calculus or the \u2200-binder of first-order logic. It also allows us to finitely axiomatize arithmetic, and similarly to axiomatize \u201cnominal\u201d datatypes-with-binding.<\/jats:p>\n          <jats:p>Just like first- and higher-order logic, equality reasoning is not necessary to \u03b1-rename.<\/jats:p>\n          <jats:p>This gives PNL much of the expressive power of higher-order logic, but models and derivations of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity.<\/jats:p>","DOI":"10.1145\/2287718.2287720","type":"journal-article","created":{"date-parts":[[2012,8,28]],"date-time":"2012-08-28T13:09:44Z","timestamp":1346159384000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Permissive-nominal logic"],"prefix":"10.1145","volume":"13","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[{"name":"INRIA, France."}]},{"given":"Murdoch J.","family":"Gabbay","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, UK"}]}],"member":"320","published-online":{"date-parts":[[2012,8,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25984-8_34"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.05.012"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_24"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836111"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 24th Italian Conference on Computational Logic (CILC'09)","author":"Dowek G.","unstructured":"Dowek , G. , Gabbay , M. J. , and Mulligan , D. P . 2009. Permissive nominal terms and their unification . In Proceedings of the 24th Italian Conference on Computational Logic (CILC'09) . Dowek, G., Gabbay, M. J., and Mulligan, D. P. 2009. Permissive nominal terms and their unification. In Proceedings of the 24th Italian Conference on Computational Logic (CILC'09)."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzq006"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '02)","author":"Dowek G.","unstructured":"Dowek , G. , Hardin , T. , and Kirchner , C . 2002. Binding logic: Proofs and models . In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '02) . Springer, 130--144. Dowek, G., Hardin, T., and Kirchner, C. 2002. Binding logic: Proofs and models. In Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '02). Springer, 130--144."},{"key":"e_1_2_1_10_1","volume-title":"Elements of Intuitionism","author":"Dummett M.","unstructured":"Dummett , M. 1977. Elements of Intuitionism 1 st Ed. Clarendon Press . Dummett, M. 1977. Elements of Intuitionism 1st Ed. Clarendon Press.","edition":"1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2007.11.001"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1305810770"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1069774.1069783"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.012"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.010"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn055"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1305810911"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000272"},{"key":"e_1_2_1_21_1","volume-title":"Handbook of Philosophical Logic.","author":"Gabbay M. J.","unstructured":"Gabbay , M. J. 2012. Nominal terms and nominal logics: from foundations to meta-mathematics . In Handbook of Philosophical Logic. Vol. 17 , Kluwer . Gabbay, M. J. 2012. Nominal terms and nominal logics: from foundations to meta-mathematics. In Handbook of Philosophical Logic. Vol. 17, Kluwer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021850"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770176.1770188"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0056-1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm064"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp033"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming (TAASN '09)","author":"Gabbay M. J.","unstructured":"Gabbay , M. J. and Mulligan , D. P . 2009a. Semantic nominal terms . In Proceedings of the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming (TAASN '09) . Gabbay, M. J. and Mulligan, D. P. 2009a. Semantic nominal terms. In Proceedings of the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming (TAASN '09)."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577835"},{"key":"e_1_2_1_29_1","first-page":"3","article-title":"A New Approach to Abstract Syntax with Variable Binding","volume":"13","author":"Gabbay M. J.","year":"2001","unstructured":"Gabbay , M. J. and Pitts , A. M. 2001 . A New Approach to Abstract Syntax with Variable Binding . Formal Aspects Comput 13 , 3 -- 5 , 341--363. Gabbay, M. J. and Pitts, A. M. 2001. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput 13, 3--5, 341--363.","journal-title":"Formal Aspects Comput"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.33"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10). Leibniz International Proceedings in Informatics (LIPIcs) Series","volume":"6","author":"Levy J.","unstructured":"Levy , J. and Villaret , M . 2010. An efficient nominal unification algorithm . In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10). Leibniz International Proceedings in Informatics (LIPIcs) Series , vol. 6 , Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 209--226. Levy, J. and Villaret, M. 2010. An efficient nominal unification algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10). Leibniz International Proceedings in Informatics (LIPIcs) Series, vol. 6, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 209--226."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS","author":"Miller D.","year":"2003","unstructured":"Miller , D. and Tiu , A . 2003. A proof theory for generic judgments (extended abstract) . In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003 ). IEEE Computer Society Press, 118--127. Miller, D. and Tiu, A. 2003. A proof theory for generic judgments (extended abstract). In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003). IEEE Computer Society Press, 118--127."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_34_1","volume-title":"Academic","author":"Paulson L. C.","unstructured":"Paulson , L. C. 1990. Isabelle: the next 700 theo rem provers . In Logic and Computer Science, P. Odifreddi, Ed. Academic Press , 361--386. Paulson, L. C. 1990. Isabelle: the next 700 theo rem provers. In Logic and Computer Science, P. Odifreddi, Ed. Academic Press, 361--386."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_2_1_36_1","volume-title":"Mathematical Logic","author":"Shoenfield J.","unstructured":"Shoenfield , J. 1967. Mathematical Logic . Addison-Wesley . Shoenfield, J. 1967. Mathematical Logic. Addison-Wesley."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.016"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2287718.2287720","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2287718.2287720","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:04Z","timestamp":1750236544000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2287718.2287720"}},"subtitle":["First-order logic over nominal terms and sets"],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2287718.2287720"],"URL":"https:\/\/doi.org\/10.1145\/2287718.2287720","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2010-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-08-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}