{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:47:07Z","timestamp":1761598027583},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T00:00:00Z","timestamp":1546819200000},"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":["J Intell Robot Syst"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10846-018-0971-9","type":"journal-article","created":{"date-parts":[[2019,1,6]],"date-time":"2019-01-06T20:26:48Z","timestamp":1546806408000},"page":"179-191","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Robotic Task Planning Using a Backchaining Theorem Prover for Multiplicative Exponential First-Order Linear Logic"],"prefix":"10.1007","volume":"96","author":[{"given":"Sitar","family":"Kortik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uluc","family":"Saranli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,1,7]]},"reference":[{"issue":"3","key":"971_CR1","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1109\/TRO.2011.2178134","volume":"28","author":"O Arslan","year":"2012","unstructured":"Arslan, O., Saranli, U.: Reactive planning and control of planar spring-mass running on rough terrain. IEEE Trans. Robot. 28(3), 567\u2013579 (2012)","journal-title":"IEEE Trans. Robot."},{"issue":"1","key":"971_CR2","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MRA.2007.339624","volume":"14","author":"C Belta","year":"2007","unstructured":"Belta, C., Bicchi, A., Egerstedt, M., Frazzoli, E., Klavins, E., Pappas, G.: Symbolic planning and control of robot motion - grand challenges of robotics. IEEE Robot. Autom. Mag. 14(1), 61\u201370 (2007)","journal-title":"IEEE Robot. Autom. Mag."},{"key":"971_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2015.06.019","volume":"597","author":"K Bimb\u00f3","year":"2015","unstructured":"Bimb\u00f3, K.: The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci. 597, 1\u201317 (2015)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"971_CR4","first-page":"1636","volume":"90","author":"AL Blum","year":"1995","unstructured":"Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1), 1636\u20131642 (1995)","journal-title":"Artif. Intell."},{"key":"971_CR5","volume-title":"Knowledge Representation and Reasoning","author":"R Brachman","year":"2004","unstructured":"Brachman, R., Levesque, H.: Knowledge Representation and Reasoning. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"issue":"1-2","key":"971_CR6","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00173-5","volume":"232","author":"I Cervesato","year":"2000","unstructured":"Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theor. Comput. Sci. 232(1-2), 133\u2013163 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"971_CR7","unstructured":"Chrpa, L.: Linear logic in planning. In: Proceedings of the International Conference on Automated Planning and Scheduling, pp. 26\u201329 (2006)"},{"issue":"1","key":"971_CR8","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1109\/TRO.2008.2008738","volume":"25","author":"D Conner","year":"2009","unstructured":"Conner, D., Choset, H., Rizzi, A.: Flow-through policies for hybrid controller synthesis applied to fully actuated systems. IEEE Trans. Robot. 25(1), 136\u2013146 (2009)","journal-title":"IEEE Trans. Robot."},{"key":"971_CR9","doi-asserted-by":"crossref","unstructured":"Dimopoulos, Y., Nebel, B., Koehler, J.: Encoding planning problems in nonmonotonic logic programs. In: Steel, S., Alami, R. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, pp. 169\u2013181. Springer (1348)","DOI":"10.1007\/3-540-63912-8_84"},{"key":"971_CR10","unstructured":"Dixon, L., Bundy, A., Smaill, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: Proceedings of the Workshop on Verification and Validation of Planning and Scheduling Systems, p. 10 (2009)"},{"key":"971_CR11","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10849-008-9079-0","volume":"18","author":"L Dixon","year":"2009","unstructured":"Dixon, L., Smaill, A., Tsang, T.: Plans, actions and dialogue using linear logic. J. Log. Lang. Inf. 18, 251\u2013289 (2009)","journal-title":"J. Log. Lang. Inf."},{"issue":"2","key":"971_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0004-3702(01)00128-X","volume":"132","author":"MB Do","year":"2001","unstructured":"Do, M.B., Kambhampati, S.: Planning as constraint satisfaction: Solving the planning graph by compiling it into CSP. Artif. Intell. 132(2), 151\u2013182 (2001)","journal-title":"Artif. Intell."},{"key":"971_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1613\/jair.1148","volume":"19","author":"T Eiter","year":"2003","unstructured":"Eiter, T., Faber, W., Leone, N., Pfeifer, G., Polleres, A.: Answer set planning under action costs. J. Artif. Intell. Res. 19, 25\u201371 (2003)","journal-title":"J. Artif. Intell. Res."},{"issue":"1","key":"971_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"issue":"2-3","key":"971_CR15","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0004-3702(92)90028-V","volume":"56","author":"N Gupta","year":"1992","unstructured":"Gupta, N., Nau, D.S.: On the complexity of blocks-world planning. Artif. Intell. 56(2-3), 223\u2013254 (1992)","journal-title":"Artif. Intell."},{"issue":"2","key":"971_CR16","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"JS Hodas","year":"1994","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110 (2), 327\u2013365 (1994)","journal-title":"Inf. Comput."},{"key":"971_CR17","unstructured":"Jacopin, E.: Classical AI planning as theorem proving: the case of a fragment of linear logic. In: AAAI Fall Symposium on Automated Deduction in Nonstandard Logics, Palo Alto, CA (1993)"},{"key":"971_CR18","unstructured":"Kahramanogullari, O.: Towards planning as concurrency. In: Artificial Intelligence and Applications, pp. 387\u2013393 (2005)"},{"key":"971_CR19","doi-asserted-by":"crossref","unstructured":"Kahramano\u011fullar\u0131, O.: On linear logic planning and concurrency. In: Language and Automata Theory and Applications, pp. 250\u2013262. Springer (2008)","DOI":"10.1007\/978-3-540-88282-4_24"},{"issue":"6","key":"971_CR20","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1017\/S0960129501003413","volume":"11","author":"M Kanovich","year":"2001","unstructured":"Kanovich, M., Vauzeilles, J.: The classical AI planning problems in the mirror of horn linear logic: semantics, expressibility, complexity. Math. Struct. Comput. Sci. 11(6), 689\u2013716 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"20","key":"971_CR21","doi-asserted-by":"publisher","first-page":"2072","DOI":"10.1016\/j.tcs.2010.12.027","volume":"412","author":"MI Kanovich","year":"2011","unstructured":"Kanovich, M.I., Vauzeilles, J.: Linear logic as a tool for planning under temporal uncertainty. Theor. Comput. Sci. 412(20), 2072\u20132092 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"971_CR22","doi-asserted-by":"crossref","unstructured":"Kortik, S., Saranli, U.: Linear planning logic: an efficient language and theorem prover for robotic task planning. In: Proceedings of the IEEE International Conference on Robotics and Automation, pp. 3764\u20133770 (2014)","DOI":"10.1109\/ICRA.2014.6907404"},{"key":"971_CR23","unstructured":"Kungas, P.: Linear Logic Programming for AI Planning. M.Sc., Institute of Cybernetic at Tallinn Technical University (2002)"},{"key":"971_CR24","doi-asserted-by":"crossref","unstructured":"LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)","DOI":"10.1017\/CBO9780511546877"},{"key":"971_CR25","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1613\/jair.3489","volume":"43","author":"J Lee","year":"2012","unstructured":"Lee, J., Palla, R.: Reformulating the situation calculus and the event calculus in the general theory of stable models and in answer set programming. J. Artif. Intell. Res. 43, 571\u2013620 (2012)","journal-title":"J. Artif. Intell. Res."},{"key":"971_CR26","doi-asserted-by":"crossref","unstructured":"Lifschitz, V.: Answer set planning. In: Gelfond, M., Leone, N., Pfeifer, G. (eds.) Logic Programming and Nonmonotonic Reasoning, Lecture Notes in Computer Science, vol. 1730, pp. 373\u2013374. Springer (1999)","DOI":"10.1007\/3-540-46767-X_28"},{"key":"971_CR27","unstructured":"Lopez, A., Bacchus, F.: Generalizing GraphPlan by formulating planning as a CSP. In: Proceedings of the International Joint Confernece on Artificial Intelligence, pp. 954\u2013960. Morgan Kaufmann Publishers Inc., San Francisco (2003)"},{"key":"971_CR28","unstructured":"Lozano-Perez, T.: Task planning. In: Robot Motion Planning and Control, pp. 473\u2013498. MIT Press, Cambridge (1982)"},{"key":"971_CR29","doi-asserted-by":"crossref","unstructured":"Mantel, H., Otten, J.: lintap: a tableau prover for linear logic. In: Automated Reasoning with Analytic Tableaux and Related Methods, pp. 661\u2013661 (1999)","DOI":"10.1007\/3-540-48754-9_20"},{"key":"971_CR30","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.engappai.2014.11.004","volume":"39","author":"D Mart\u00ednez","year":"2015","unstructured":"Mart\u00ednez, D, Aleny\u00e1\u00e1, G., Torras, C.: Planning robot manipulation to clean planar surfaces. Eng. Appl. Artif. Intell. 39, 23\u201332 (2015)","journal-title":"Eng. Appl. Artif. Intell."},{"issue":"2","key":"971_CR31","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0304-3975(93)90007-G","volume":"113","author":"M Masseron","year":"1993","unstructured":"Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic I. Actions as proofs. Theor. Comput. Sci. 113(2), 349\u2013370 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"971_CR32","unstructured":"McAllester, D., Rosenblitt, D.: Systematic nonlinear planning. In: Proceedings of the National Conference of the American Association for Artificial Intelligence (AAAI-91), pp. 634\u2013639 (1991)"},{"key":"971_CR33","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: Situations, Actions, and Causal Laws. Tech. Rep AD0785031. Stanford University, Department of Computer Science (1963)","DOI":"10.21236\/AD0785031"},{"issue":"4","key":"971_CR34","first-page":"43","volume":"28","author":"DS Nau","year":"2007","unstructured":"Nau, D.S.: Current trends in automated planning. AI Mag. 28(4), 43 (2007)","journal-title":"AI Mag."},{"key":"971_CR35","unstructured":"Penberthy, J.S., Weld, D.S.: UCPOP: a sound, complete, partial order planner for ADL. In: Proceedings of the International Conference on Knowledge Representation and Reasoning, pp. 103\u2013114 (1992)"},{"key":"971_CR36","unstructured":"Pfenning, F.: Lecture Notes on Automated Theorem Proving. Technical report, Carnegie Mellon University (1999)"},{"key":"971_CR37","unstructured":"Pfenning, F.: Lecture Notes on Linear Logic. Technical report, Carnegie Mellon University (2002)"},{"key":"971_CR38","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/B978-0-12-450010-5.50026-8","volume":"27","author":"R Reiter","year":"1991","unstructured":"Reiter, R.: The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. Artif. Intell. Math. Theory Comput. 27, 359\u2013380 (1991)","journal-title":"Artif. Intell. Math. Theory Comput."},{"key":"971_CR39","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Prentice Hall, Englewood Cliffs (2003)"},{"issue":"7","key":"971_CR40","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1177\/02783640122067570","volume":"20","author":"U Saranli","year":"2001","unstructured":"Saranli, U., Buehler, M., Koditschek, D.E.: RHex: a simple and highly mobile robot. Int. J. Robot. Res. 20(7), 616\u2013631 (2001)","journal-title":"Int. J. Robot. Res."},{"key":"971_CR41","volume-title":"User\u2019s Guide of a Linear Logic Theorem Prover (Llprover). Tech. Rep., Department of Computer and Systems Engineering Faculty of Engineering","author":"N Tamura","year":"1998","unstructured":"Tamura, N.: User\u2019s Guide of a Linear Logic Theorem Prover (Llprover). Tech. Rep., Department of Computer and Systems Engineering Faculty of Engineering. Kobe University, Japan (1998)"},{"key":"971_CR42","volume-title":"Type Theory and Functional Programming","author":"S Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. Addison-Wesley, Reading (1991)"},{"issue":"8","key":"971_CR43","doi-asserted-by":"publisher","first-page":"1967","DOI":"10.1016\/j.engappai.2013.04.006","volume":"26","author":"TS Vaquero","year":"2013","unstructured":"Vaquero, T.S., Silva, J.R., Beck, J.C.: Post-design analysis for building and refining AI planning systems. Eng. Appl. Artif. Intell. 26(8), 1967\u20131979 (2013)","journal-title":"Eng. Appl. Artif. Intell."}],"container-title":["Journal of Intelligent & Robotic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10846-018-0971-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10846-018-0971-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10846-018-0971-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T19:09:53Z","timestamp":1578337793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10846-018-0971-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,7]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["971"],"URL":"https:\/\/doi.org\/10.1007\/s10846-018-0971-9","relation":{},"ISSN":["0921-0296","1573-0409"],"issn-type":[{"value":"0921-0296","type":"print"},{"value":"1573-0409","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,7]]},"assertion":[{"value":"13 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}