{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T21:32:14Z","timestamp":1672349534235},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bf00881831","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T16:11:47Z","timestamp":1104163907000},"page":"69-93","source":"Crossref","is-referenced-by-count":1,"title":["Mechanical verification of strategies"],"prefix":"10.1007","volume":"15","author":[{"given":"Sakthi","family":"Subramanian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Readings in Planning","year":"1990","unstructured":"Allen, J., Hendler, J., and Tate, A., eds:Readings in Planning, Morgan Kaufmann, San Mateo, CA, 1990."},{"issue":"4","key":"CR2","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W. Bevier","year":"1989","unstructured":"Bevier, W., Hunt, W., Moore, J. S., and Young, W.: An approach to systems verification,J. Automated Reasoning 5(4) (1989), 411?428.","journal-title":"J. Automated Reasoning"},{"key":"CR3","unstructured":"Boyer, R. S. and Moore, J. S.:A Computational Logic Handbook: Authorized Excepts from a Proposed, 2nd edn, Available electronically by anonymous ftp from ftp.cli.com along with Nqthm-1992."},{"key":"CR4","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-1-4612-4476-9_7","volume-title":"Beauty Is Our Business: A Birthday Salute to Edger W. Dijkstra, Texts and Monographs in Computer Science","author":"R. S. Boyer","year":"1990","unstructured":"Boyer, R. S., Moore, J. S., and Green, M. W.: The use of a formal simulator to verify a simple real time control program, inBeauty Is Our Business: A Birthday Salute to Edger W. Dijkstra, Texts and Monographs in Computer Science, Springer, Berlin, 1990, pp. 54?66."},{"key":"CR5","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S., and Moore, J. S.:A Computational Logic Handbook, Academic Press, New York, 1988."},{"key":"CR6","volume-title":"Readings in Knowledge Representation","year":"1985","unstructured":"Brachman, R. and Levesque, H., eds:Readings in Knowledge Representation, Morgan Kaufmann, San Mateo, CA, 1985."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam System, Technical Report DAI Research Paper No. 507, Department of Artificial Intelligence, University of Edinburgh, 1990.","DOI":"10.1007\/3-540-52885-7_123"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(74)90008-3","volume":"5","author":"S. Fahlman","year":"1974","unstructured":"Fahlman, S.: A planning system for robot construction tasks,Artificial Intelligence 5 (1974), 1?49.","journal-title":"Artificial Intelligence"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R. E. Fikes","year":"1971","unstructured":"Fikes, R. E. and Nilsson, N. J.: STRIPS: A new approach to the application of theorem proving to problem solving,Artificial Intelligence 2 (1971), 189?208.","journal-title":"Artificial Intelligence"},{"key":"CR10","volume-title":"Logical Foundations of Artificial Intelligence","author":"M. R. Genesereth","year":"1987","unstructured":"Genesereth, M. R. and Nilsson, N. J.:Logical Foundations of Artificial Intelligence, Morgan Kaufmann, Los Altos, CA, 1987."},{"key":"CR11","volume-title":"Readings in Artificial Intelligence","author":"C. Green","year":"1981","unstructured":"Green, C.: Application of theorem proving to problem solving, in B. L. Webber and N. J. Nilsson (eds),Readings in Artificial Intelligence, Morgan Kaufmann, Los Altos, CA, 1981."},{"key":"CR12","first-page":"495","volume-title":"Machine Intelligence, Vol. 6","author":"P. J. Hayes","year":"1971","unstructured":"Hayes, P. J.: A logic of actions, in D. Michie and B. Meltzer (eds),Machine Intelligence, Vol. 6, Wiley, New York, 1971, pp. 495?520."},{"key":"CR13","unstructured":"Kaufmann, M.: Proof script available electronically by anonymous ftp from ftp.cli.com along with Pc-Nqthm-1992."},{"key":"CR14","unstructured":"Kaufmann, M.: A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Technical Report 19, Computational Logic, Inc., May 1988."},{"key":"CR15","first-page":"140","volume-title":"Readings in Planning","author":"F. Kluzniak","year":"1990","unstructured":"Kluzniak, F. and Szpakowicz, S.: Extract from Prolog for Programmers, in J. Allen, J. Hendler, and A. Tate (eds),Readings in Planning, Morgan Kaufmann, San Mateo, CA, 1990, pp. 140?153."},{"key":"CR16","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/BF00247434","volume":"3","author":"Z. Manna","year":"1987","unstructured":"Manna, Z. and Waldinger, R.: How to clear a block: A theory of plans,J. Automated Reasoning 3 (1987), 343?377.","journal-title":"J. Automated Reasoning"},{"key":"CR17","unstructured":"McAllester, D. and Rosenblitt, D.: Systematic nonlinear planning, inProc. of AAAI-91, pp. 634?639."},{"key":"CR18","volume-title":"Semantic Information Processing","author":"J. McCarthy","year":"1968","unstructured":"McCarthy, J.: Programs with common sense, ch. 7 in M. Minsky (ed.),Semantic Information Processing, MIT Press, Cambridge, MA, 1968."},{"key":"CR19","volume-title":"Machine Intelligence, Vol. 4","author":"J. McCarthy","year":"1969","unstructured":"McCarthy, J. and Hayes, P.: Some philosophical problems from the standpoint of artificial intelligence, in D. Michie and B. Meltzer (eds),Machine Intelligence, Vol. 4, Edinburgh University Press, Edinburgh, Scotland, 1969."},{"key":"CR20","volume-title":"Semantic Information Processing","year":"1968","unstructured":"Minsky, M., ed.:Semantic Information Processing, MIT Press, Cambridge, MA, 1968."},{"key":"CR21","first-page":"245","volume-title":"Readings in Knowledge Representation","author":"M. Minsky","year":"1985","unstructured":"Minsky, M.: A framework for representing knowledge, in R. Brachman and H. Levesque (eds),Readings in Knowledge Representation, Morgan Kaufmann, San Mateo, CA, 1985, pp. 245?262."},{"key":"CR22","unstructured":"Minton, S., Knoblock, C. A., Kuokka, D. R., Gil, Y., Joseph, R. L., and Carbonell, J. G.: Prodigy 2.0: The Manual and Tutorial. Technical Report CMU-CS-89-146, School of Computer Science, Carnegie Mellon University, May 1989."},{"key":"CR23","unstructured":"Moore, J. S.: Proof script available electronically by anonymous ftp from ftp.cli.com along with Nqthm-1992."},{"key":"CR24","volume-title":"Principles of Artificial Intelligence","author":"N. J. Nilsson","year":"1980","unstructured":"Nilsson, N. J.:Principles of Artificial Intelligence, Springer, New York, 1980."},{"key":"CR25","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1111\/j.1467-8640.1988.tb00285.x","volume":"4","author":"E. P. D. Pednault","year":"1988","unstructured":"Pednault, E. P. D.: Synthesizing plans that contain actions with context-dependent effects,Computational Intelligence 4 (1988), 356?372.","journal-title":"Computational Intelligence"},{"key":"CR26","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1016\/B978-0-12-450010-5.50026-8","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","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, in V. Lifschitz (ed.),Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, London, 1991, pp. 359?380."},{"key":"CR27","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-94-009-0553-5_2","volume-title":"Knowledge Representation and Defeasible Reasoning","author":"L. Schubert","year":"1990","unstructured":"Schubert, L.: Monotonic solution of the frame problem in the situation calculus: an efficient method for worlds with fully specified actions, in H. E. Kyburg, R. Loui, and G. Carlson (eds),Knowledge Representation and Defeasible Reasoning, Kluwer, Dordrecht 1990, pp. 23?67."},{"key":"CR28","unstructured":"Stephan, W. and Biundo, S.: A new logical framework for deductive planning, inProc. of IJCAI-93."},{"key":"CR29","unstructured":"Subramanian, S.: A Mechanized Framework for Specifying Problem Domains and Verifying Plans, Ph.D. Thesis, University of Texas, Austin, Department of Computer Science, 1993."},{"key":"CR30","first-page":"26","volume-title":"Readings in Planning","author":"A. Tate","year":"1990","unstructured":"Tate, A., Hendler, J., and Drummond, M.: A review of AI planning techniques, in J. Allen, J. Hendler and A. Tate (eds),Readings in Planning, Morgan Kaufmann, San Mateo, CA, 1990, pp. 26?50."},{"key":"CR31","volume-title":"Readings in Artificial Intelligence","author":"R. J. Waldinger","year":"1981","unstructured":"Waldinger, R. J.: Achieving several goals simultaneously, in B. L. Webber and N. J. Nilsson (eds),Readings in Artificial Intelligence, Morgan Kaufmann, Los Altos, CA, 1981."},{"key":"CR32","first-page":"697","volume-title":"Lecture Notes in Computer Science","author":"M. Wilding","year":"1993","unstructured":"Wilding, M.: A mechanically verified application for a mechanically verified environment, inLecture Notes in Computer Science, 697. Springer, Berlin, 1993. Also available by anonymous ftp from ftp.cli.com along with Nqthm-1992."},{"key":"CR33","volume-title":"Computer Models of Thought and Language","author":"T. Winograd","year":"1973","unstructured":"Winograd, T.: A procedural model of language understanding, in R. Schank and K. Colby (eds),Computer Models of Thought and Language, Freeman, San Francisco, 1973."},{"key":"CR34","first-page":"357","volume-title":"Readings in Knowledge Representation","author":"T. Winograd","year":"1985","unstructured":"Winograd, T.: Frame representations and the declarative\/ptocedural controversy, in R. Brachman and H. Levesque (eds),Readings in Knowledge Representation, Morgan Kaufmann, San Mateo, CA, 1985, pp. 357?370."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881831.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881831\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881831","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:07:28Z","timestamp":1586045248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881831"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995]]}},"alternative-id":["BF00881831"],"URL":"https:\/\/doi.org\/10.1007\/bf00881831","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}