{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:25:41Z","timestamp":1750220741302,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T00:00:00Z","timestamp":1599523200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,8]]},"DOI":"10.1145\/3414080.3414094","type":"proceedings-article","created":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T23:11:58Z","timestamp":1600729918000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Proof-Carrying Plans: a Resource Logic for AI Planning"],"prefix":"10.1145","author":[{"given":"Alasdair","family":"Hill","sequence":"first","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronald P. A.","family":"Petrick","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,9,21]]},"reference":[{"volume-title":"10th International Conference on Interactive Theorem Proving (ITP","year":"2019","author":"Abdulaziz Mohammad","key":"e_1_3_2_1_1_1"},{"key":"e_1_3_2_1_2_1","unstructured":"aibasel. 2020. Downward Benchmarks. https:\/\/github.com\/aibasel\/downward-benchmarks  aibasel. 2020. Downward Benchmarks. https:\/\/github.com\/aibasel\/downward-benchmarks"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00044-3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem Klaus Havelund and Andrea Orlandini. 2014. Verification and validation meet planning and scheduling.  Saddek Bensalem Klaus Havelund and Andrea Orlandini. 2014. Verification and validation meet planning and scheduling.","DOI":"10.1007\/s10009-013-0294-x"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"volume-title":"Applications of Declarative Programming and Knowledge Management","author":"Chrpa Luk\u00e1\u0161","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","unstructured":"Daniel\u00a0C Dennett. 2006. Cognitive wheels: The frame problem of AI. (2006).  Daniel\u00a0C Dennett. 2006. Cognitive wheels: The frame problem of AI. (2006)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-008-9079-0"},{"volume-title":"GPS: A case study in generality and problem solving","year":"1969","author":"Ernst W","key":"e_1_3_2_1_11_1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622876.1622939"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Kathleen Fisher John Launchbury and Raymond Richards. 2017. The HACMS program: using formal methods to eliminate exploitable bugs. Phil. Trans. Royal Society(2017). Issue A 375.  Kathleen Fisher John Launchbury and Raymond Richards. 2017. The HACMS program: using formal methods to eliminate exploitable bugs. Phil. Trans. Royal Society(2017). Issue A 375.","DOI":"10.1098\/rsta.2015.0401"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1129"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0403-1"},{"volume-title":"FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings(Lecture Notes in Computer Science), Vol.\u00a09613","year":"2016","author":"Fu Peng","key":"e_1_3_2_1_16_1"},{"key":"e_1_3_2_1_17_1","unstructured":"Cordell Green. 1969. Theorem proving by resolution as a basis for question-answering systems. Machine intelligence 4(1969) 183\u2013205.  Cordell Green. 1969. Theorem proving by resolution as a basis for question-answering systems. Machine intelligence 4(1969) 183\u2013205."},{"volume-title":"Readings in Artificial Intelligence","author":"Hayes J","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","unstructured":"James\u00a0A Hendler Austin Tate and Mark Drummond. 1990. AI planning: Systems and techniques. AI magazine 11 2 (1990) 61\u201361.  James\u00a0A Hendler Austin Tate and Mark Drummond. 1990. AI planning: Systems and techniques. AI magazine 11 2 (1990) 61\u201361."},{"key":"e_1_3_2_1_20_1","unstructured":"A. Hill. 2020. PCP Logic: Agda formalisation. https:\/\/github.com\/PDTypes\/PCPLogic  A. Hill. 2020. PCP Logic: Agda formalisation. https:\/\/github.com\/PDTypes\/PCPLogic"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2004.120"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"volume-title":"AAAI Fall Symposium on Automated Deduction in Nonstandard Logics. AAAI Press Publications Palo Alto, CA, 62\u201366","year":"1993","author":"Jacopin Eric","key":"e_1_3_2_1_25_1"},{"key":"e_1_3_2_1_26_1","unstructured":"Xavier Leroy 2012. The CompCert verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt 53 (2012).  Xavier Leroy 2012. The CompCert verified compiler. Documentation and user\u2019s manual. INRIA Paris-Rocquencourt 53 (2012)."},{"volume-title":"Proc. Workshop on V&V of Planning and Scheduling Systems.","year":"2009","author":"Long Derek","key":"e_1_3_2_1_27_1"},{"volume-title":"Readings in artificial intelligence","author":"McCarthy John","key":"e_1_3_2_1_28_1"},{"key":"e_1_3_2_1_29_1","unstructured":"Drew McDermott Malik Ghallab Adele Howe Craig Knoblock Ashwin Ram Manuela Veloso Daniel Weld and David Wilkins. 1998. PDDL-the planning domain definition language. (1998).  Drew McDermott Malik Ghallab Adele Howe Craig Knoblock Ashwin Ram Manuela Veloso Daniel Weld and David Wilkins. 1998. PDDL-the planning domain definition language. (1998)."},{"key":"e_1_3_2_1_30_1","unstructured":"Aleksandar Nanevski. [n.d.]. Separation Logic and Concurrency.  Aleksandar Nanevski. [n.d.]. Separation Logic and Concurrency."},{"key":"e_1_3_2_1_31_1","unstructured":"Aleks Nanevski. [n.d.]. Separation Logic and Concurrency (OPLSS 2016) Draft of July 22 2016. ([n.\u00a0d.]).  Aleks Nanevski. [n.d.]. Separation Logic and Concurrency (OPLSS 2016) Draft of July 22 2016. ([n.\u00a0d.])."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"edition":"2","volume-title":"Encyclopedia of Cryptography and Security","author":"Necula C.","key":"e_1_3_2_1_34_1"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Peter\u00a0W O\u2019hearn. 2007. Resources concurrency and local reasoning. Theoretical computer science 375 1-3 (2007) 271\u2013307.  Peter\u00a0W O\u2019hearn. 2007. Resources concurrency and local reasoning. Theoretical computer science 375 1-3 (2007) 271\u2013307.","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_1_37_1","first-page":"103","article-title":"UCPOP: A Sound, Complete","volume":"92","author":"Penberthy J\u00a0Scott","year":"1992","journal-title":"Partial Order Planner for ADL.Kr"},{"volume-title":"Proceedings of the 23rd Annual Software Engineering Workshop, NASA Goddard.","year":"1998","author":"Penix John","key":"e_1_3_2_1_38_1"},{"key":"e_1_3_2_1_39_1","unstructured":"Jeff Polakow and Frank Pfenning. 2001. Ordered linear logic and applications. Carnegie Mellon University Pittsburgh.  Jeff Polakow and Frank Pfenning. 2001. Ordered linear logic and applications. Carnegie Mellon University Pittsburgh."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3326938.3326940"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_5"},{"volume-title":"Automated Reasoning, 4th International Joint Conference, IJCAR","year":"2008","author":"Schack-Nielsen Anders","key":"e_1_3_2_1_44_1"},{"volume-title":"Proof-Carrying Plans. In International Symposium on Practical Aspects of Declarative Languages. Springer, 204\u2013220","year":"2019","author":"Schwaab Christopher","key":"e_1_3_2_1_45_1"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"C. Scwaab A. Hill F. Farka and E. Komendantskaya. 2018. Proof-Carrying plans: Agda implementation and examples. https:\/\/github.com\/PDTypes  C. Scwaab A. Hill F. Farka and E. Komendantskaya. 2018. Proof-Carrying plans: Agda implementation and examples. https:\/\/github.com\/PDTypes","DOI":"10.1007\/978-3-030-05998-9_13"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020820000972"},{"key":"e_1_3_2_1_48_1","unstructured":"David\u00a0E Wilkins. 2014. Practical planning: extending the classical AI planning paradigm. Elsevier.  David\u00a0E Wilkins. 2014. Practical planning: extending the classical AI planning paradigm. Elsevier."}],"event":{"name":"PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP '20","location":"Bologna Italy"},"container-title":["Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3414080.3414094","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3414080.3414094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:38Z","timestamp":1750199918000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3414080.3414094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,8]]},"references-count":48,"alternative-id":["10.1145\/3414080.3414094","10.1145\/3414080"],"URL":"https:\/\/doi.org\/10.1145\/3414080.3414094","relation":{},"subject":[],"published":{"date-parts":[[2020,9,8]]},"assertion":[{"value":"2020-09-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}