{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T17:14:44Z","timestamp":1775322884642,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030059972","type":"print"},{"value":"9783030059989","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,12,19]],"date-time":"2018-12-19T00:00:00Z","timestamp":1545177600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-05998-9_13","type":"book-chapter","created":{"date-parts":[[2018,12,18]],"date-time":"2018-12-18T12:05:24Z","timestamp":1545134724000},"page":"204-220","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Proof-Carrying Plans"],"prefix":"10.1007","author":[{"given":"Christopher","family":"Schwaab","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alasdair","family":"Hill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franti\u0161ek","family":"Farka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronald P. A.","family":"Petrick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joe","family":"Wells","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,19]]},"reference":[{"key":"13_CR1","unstructured":"Cla\u00dfen, J., Eyerich, P., Lakemeyer, G., Nebel, B.: Towards an integration of Golog and planning. In: Veloso, M.M. (ed.) IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, 6\u201312 January 2007, pp. 1846\u20131851 (2007)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR3","unstructured":"Dutertre, B., De Moura, L.: The Yices SMT solver. Technical report, August 2006. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"issue":"3\/4","key":"13_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R Fikes","year":"1971","unstructured":"Fikes, R., Nilsson, N.J.: STRIPS: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3\/4), 189\u2013208 (1971)","journal-title":"Artif. Intell."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Fourati, F., Bhiri, M.T., Robbana, R.: Verification and validation of PDDL descriptions using Event-B formal method. In: 2016 5th International Conference on Multimedia Computing and Systems (ICMCS), pp. 770\u2013776, September 2016","DOI":"10.1109\/ICMCS.2016.7905631"},{"issue":"3","key":"13_CR6","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s00165-016-0403-1","volume":"29","author":"P Fu","year":"2017","unstructured":"Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in horn clause logic. Formal Asp. Comput. 29(3), 453\u2013474 (2017)","journal-title":"Formal Asp. Comput."},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-29604-3_9","volume-title":"Functional and Logic Programming","author":"P Fu","year":"2016","unstructured":"Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126\u2013143. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_9"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Howey, R., Long, D., Fox, M.: VAL: automatic plan validation, continuous effects and mixed initiative planning using PDDL. In: 16th IEEE International Conference on Tools with Artificial Intelligence, pp. 294\u2013301 (2004)","DOI":"10.1109\/ICTAI.2004.120"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-45484-5_9","volume-title":"Formal Approaches to Agent-Based Systems","author":"L Khatib","year":"2001","unstructured":"Khatib, L., Muscettola, N., Havelund, K.: Verification of plan models using UPPAAL. In: Rash, J.L., Truszkowski, W., Hinchey, M.G., Rouff, C.A., Gordon, D. (eds.) FAABS 2000. LNCS, vol. 1871, pp. 114\u2013122. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45484-5_9"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0743-1066(96)00121-5","volume":"31","author":"HJ Levesque","year":"1997","unstructured":"Levesque, H.J., Reiter, R., Lesp\u00e9rance, Y., Lin, F., Scherl, R.B.: GOLOG: a logic programming language for dynamic domains. J. Logic Program. 31(1), 59\u201383 (1997)","journal-title":"J. Logic Program."},{"key":"13_CR11","unstructured":"McDermott, D., et al.: PDDL - The Planning Domain Definition Language (Version 1. 2). Technical Report CVC TR-98-003\/DCS TR-1165, Yale Center for Computational Vision and Control (1998)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Ong, L.: Higher-order model checking: an overview. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 1\u201315 (2015)","DOI":"10.1109\/LICS.2015.9"},{"key":"13_CR14","unstructured":"Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. In: ICAPS 2009 Workshop on Verification and Validation of Planning and Scheduling Systems, Thessaloniki, Greece, 20 September 2009"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-1-4684-3384-5_3","volume-title":"Logic and Data Bases","author":"R Reiter","year":"1978","unstructured":"Reiter, R.: On closed world data bases. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 55\u201376. Plenum Press, New York (1978)"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1016\/j.indag.2017.05.006","volume":"29","author":"A Schubert","year":"2018","unstructured":"Schubert, A., Urzyczyn, P.: Answer set programming in intuitionistic logic. Indagationes Mathematicae 29(1), 276\u2013292 (2018). l.E.J. Brouwer, fifty years later","journal-title":"Indagationes Mathematicae"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Scwaab, C., Hill, A., Farka, F., Komendantskaya, E.: Proof-Carrying Plans: Agda Implementation and Examples (2018). https:\/\/github.com\/PDTypes","DOI":"10.1007\/978-3-030-05998-9_13"},{"key":"13_CR18","unstructured":"Scwaab, C., et al.: Proof-Carrying Plans: Extended Version of This Paper with Appendices (2018). https:\/\/github.com\/PDTypes\/PADL19\/blob\/master\/padl-pddl-verification.pdf"},{"key":"13_CR19","volume-title":"Lectures on the Curry-Howard Isomorphism, Studies in Logic","author":"MH Sorensen","year":"2006","unstructured":"Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard Isomorphism, Studies in Logic, vol. 149. Elsevier, New York (2006)"},{"issue":"12","key":"13_CR20","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/2699407","volume":"58","author":"P Wadler","year":"2015","unstructured":"Wadler, P.: Propositions as types. Commun. ACM 58(12), 75\u201384 (2015)","journal-title":"Commun. ACM"},{"key":"13_CR21","unstructured":"Waldinger, R.J.: Achieving several goals simultaneously. Machine Intelligence 8 (1977)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Zarrie\u00df, B., Cla\u00dfen, J.: Decidable verification of GOLOG programs over non-local effect actions. In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, Arizona, USA, 12\u201317 February 2016, pp. 1109\u20131115. AAAI Press (2016)","DOI":"10.1609\/aaai.v30i1.10109"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-05998-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T16:04:56Z","timestamp":1775318696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-05998-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,19]]},"ISBN":["9783030059972","9783030059989"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-05998-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,19]]},"assertion":[{"value":"19 December 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PADL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Practical Aspects of Declarative Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"padl2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/uta.engineering\/conferences\/bi-2018\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}