{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:52:33Z","timestamp":1725663153942},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_89","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:58:20Z","timestamp":1330178300000},"page":"172-189","source":"Crossref","is-referenced-by-count":13,"title":["Modal theorem proving"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15648-8_1","volume":"193","author":"M. Abadi","year":"1985","unstructured":"M. Abadi and Z. Manna, \u201cNonclausal temporal deduction,\u201d in Logics of Programs (R. Parikh, ed.), Springer-Verlag LNCS 193, 1985, pp. 1\u201315.","journal-title":"Logics of Programs"},{"key":"15_CR2","unstructured":"M. Abadi and Z. Manna, \u201cA timely resolution,\u201d Proceedings of the Symposium on Logic in Computer Science (LICS), 1986."},{"key":"15_CR3","unstructured":"L. Fari\u00f1as del Cerro, \u201cTemporal reasoning and termination of programs,\u201d Eighth International Joint Conference on Artificial Intelligence, 1983, pp. 926\u2013929."},{"issue":"2","key":"15_CR4","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1051\/ita\/1984180201611","volume":"18","author":"L. Fari\u00f1as del Cerro","year":"1984","unstructured":"L. Fari\u00f1as del Cerro, \u201cUn principe de r\u00e9solution en logique modale,\u201d RAIRO Informatique Th\u00e9orique, Vol. 18, No. 2, 1984, pp. 161\u2013170.","journal-title":"RAIRO Informatique Th\u00e9orique"},{"key":"15_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-642-82453-1_2","volume-title":"Logics and Models of Concurrent Systems","author":"L. Fari\u00f1as del Cerro","year":"1985","unstructured":"L. Fari\u00f1as del Cerro, \u201cResolution modal logics,\u201d in Logics and Models of Concurrent Systems (K.R. Apt, ed.), Springer-Verlag, Heidelberg, 1985, pp. 27\u201355."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"M. Fitting, Proof Methods for Modal and Intuitionistic Logics, D. Reidel Publishing Co., Dordrecht, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"15_CR7","unstructured":"M. Fitting, private communication."},{"key":"15_CR8","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/B978-0-934613-04-0.50026-0","volume-title":"Theoretical Aspects of Reasoning about Knowledge","author":"C. Geissler","year":"1986","unstructured":"C. Geissler and K. Konolige, \u201cA resolution method for quantified modal logics of knowledge and belief,\u201d in Theoretical Aspects of Reasoning about Knowledge (J. Halpern, ed.), Morgan Kaufmann Publishers, Palo Alto, 1986, pp. 309\u2013324."},{"key":"15_CR9","volume-title":"An Introduction to Modal Logic","author":"G.E. Hughes","year":"1968","unstructured":"G.E. Hughes and M.J. Cresswell, An Introduction to Modal Logic, Methuen & Co., London, 1968."},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"J.Y. Halpern and Y. Moses, \u201cKnowledge and Common Knowledge in a Distributed Environment,\u201d Third ACM Conference on the Principles of Distributed Computing, 1984, pp. 50\u201361. A revised version appears as IBM RJ 4421, 1984.","DOI":"10.1145\/800222.806735"},{"key":"15_CR11","unstructured":"K. Konolige, A Deduction Model of Belief and its Logics, Ph.D. Thesis, Computer Science Department, Stanford University, 1984."},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/322290.322293","volume":"29","author":"D. McDermott","year":"1982","unstructured":"D. McDermott, \u201cNonmonotonic Logic II: Nonmonotonic Modal Theories,\u201d Journal of the ACM, Vol. 29, No. 1, Jan. 1982, pp. 33\u201357.","journal-title":"Journal of the ACM"},{"issue":"1","key":"15_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","volume":"18","author":"N.V. Murray","year":"1982","unstructured":"N.V. Murray, \u201cCompletely nonclausal theorem proving,\u201d Artificial Intelligence, Vol. 18, No. 1, January 1982, pp. 67\u201385.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"15_CR14","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna and R. Waldinger, \u201cA deductive approach to program synthesis,\u201d ACM Transactions on Programming, Languages, and Systems, Vol. 2, No. 1, Jan. 1980, pp. 90\u2013121.","journal-title":"ACM Transactions on Programming, Languages, and Systems"},{"issue":"1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/4904.4905","volume":"33","author":"Z. Manna","year":"1986","unstructured":"Z. Manna and R. Waldinger, \u201cSpecial relations in automated deduction,\u201d Journal of the ACM, Vol. 33, No. 1, Jan. 1986, pp. 1\u201359.","journal-title":"Journal of the ACM"},{"key":"15_CR16","unstructured":"Z. Manna and R. Waldinger, \u201cSpecial relations in program-synthetic deduction,\u201d Report No. STAN-CS-82-902, Computer Science Department, Stanford University, March 1982."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cThe temporal logic of programs,\u201d 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, \u201cA machine-oriented logic based on the resolution principle,\u201d Journal of the ACM, Vol. 12, No. 1, January 1965, pp. 23\u201341.","journal-title":"Journal of the ACM"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"P. Wolper, \u201cTemporal Logic can be more expressive,\u201d 22nd Annual Symposium on Foundations of Computer Science, 1981, pp. 340\u2013348.","DOI":"10.1109\/SFCS.1981.44"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_89.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T17:07:22Z","timestamp":1619543242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_89"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_89","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}