{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:24:35Z","timestamp":1742981075909,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642376504"},{"type":"electronic","value":"9783642376511"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37651-1_13","type":"book-chapter","created":{"date-parts":[[2013,4,5]],"date-time":"2013-04-05T00:10:01Z","timestamp":1365120601000},"page":"302-316","source":"Crossref","is-referenced-by-count":3,"title":["Planning with Effectively Propositional Logic"],"prefix":"10.1007","author":[{"given":"Juan Antonio","family":"Navarro-P\u00e9rez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0168-0072(92)90042-X","volume":"57","author":"M. Baaz","year":"1992","unstructured":"Baaz, M., Leitsch, A.: Complexity of resolution proofs and function introduction. Annals of Pure and Applied Logic\u00a057(3), 181\u2013215 (1992)","journal-title":"Annals of Pure and Applied Logic"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 2, pp. 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"13_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/11532231_29","volume-title":"Automated Deduction \u2013 CADE-20","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 392\u2013408. Springer, Heidelberg (2005)"},{"key":"13_CR4","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style model finding. In: MODEL 2003: Proceedings of the Workshop on Model Computation (2003)"},{"key":"13_CR5","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. Artificial Intelligence\u00a02, 189\u2013208 (1971)","journal-title":"Artificial Intelligence"},{"key":"13_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 497\u2013511. Springer, Heidelberg (2006)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Green, C.: Application of theorem proving to problem solving. In: IJCAI 1969: Proceedings of the 1st International Joint Conference on Artificial Intelligence, Washington, DC, USA, pp. 219\u2013239 (1969)","DOI":"10.21236\/ADA459656"},{"key":"13_CR8","first-page":"343","volume-title":"Proceedings of the 1987 Workshop on The Frame Problem in Artificial Intelligence","author":"A.R. Haas","year":"1987","unstructured":"Haas, A.R.: The case for domain specific frame axioms. In: Brown, F.M. (ed.) Proceedings of the 1987 Workshop on The Frame Problem in Artificial Intelligence, pp. 343\u2013348. Morgan Kaufmann, Lawrence (1987)"},{"key":"13_CR9","first-page":"359","volume-title":"ECAI 1992: Proceedings of the 10th European Conference on Artificial Intelligence","author":"H. Kautz","year":"1992","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: ECAI 1992: Proceedings of the 10th European Conference on Artificial Intelligence, pp. 359\u2013363. John Wiley & Sons, Inc, Vienna (1992)"},{"key":"13_CR10","unstructured":"Kautz, H., McAllester, D., Selman, B.: Encoding plans in propositional logic. In: KR 1996: Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning, Boston, MA, USA (1996)"},{"key":"13_CR11","unstructured":"Navarro P\u00e9rez, J.A.: Encoding and Solving Problems in Effectively Propositional Logic. PhD thesis, The University of Manchester (2007)"},{"key":"13_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-73595-3_24","volume-title":"Automated Deduction \u2013 CADE-21","author":"J.A. Navarro-P\u00e9rez","year":"2007","unstructured":"Navarro-P\u00e9rez, J.A., Voronkov, A.: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 346\u2013361. Springer, Heidelberg (2007)"},{"issue":"3","key":"13_CR13","first-page":"747","volume":"2","author":"A. David","year":"1986","unstructured":"David, A.: Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation\u00a02(3), 747\u20137171 (1986) ISSN: 0747-7171","journal-title":"Journal of Symbolic Computation"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-94-009-0553-5_2","volume-title":"Knowledge Representation and Defeasible Reasoning","author":"L.K. Schubert","year":"1990","unstructured":"Schubert, L.K.: Monotonic solution of the frame problem in the situation calculus: An efficient method for worlds with fully specified actions. In: Kyburg, H., Loui, R., Carlson, G. (eds.) Knowledge Representation and Defeasible Reasoning, pp. 23\u201367. Kluwer Academic Publishers, Dordrecht (1990)"},{"issue":"4","key":"13_CR15","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"13_CR16","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.B.: The state of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"}],"container-title":["Lecture Notes in Computer Science","Programming Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37651-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:30:25Z","timestamp":1558301425000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37651-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376504","9783642376511"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37651-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}