{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:17:16Z","timestamp":1737091036377,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_7","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:26:55Z","timestamp":1179376015000},"page":"85-99","source":"Crossref","is-referenced-by-count":12,"title":["A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"7_CR1","unstructured":"A. Artale and E. Franconi. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence. To appear."},{"key":"7_CR2","unstructured":"E. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press, 2000."},{"key":"7_CR3","unstructured":"A. Degtyarev and M. Fisher. Propositional temporal resolution revisited. In Proc. of 7th UK Workshop on Automated Reasoning (ARW), London, July 2000."},{"key":"7_CR4","unstructured":"A. Degtyarev and M. Fisher. An Extension of Propositional Temporal Resolution. In Proc. UK Workshop on Automated Reasoning (ARW), York, March 2001."},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Proc. KI 2001","author":"A. Degtyarev","year":"2001","unstructured":"A. Degtyarev and M. Fisher. Towards First-Order Temporal Resolution. In Proc. KI 2001, volume 2174 of LNCS. Springer Verlag, 2001."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"R. Fagin, J. Halpern, Y. Moses, and M. Vardi. Reasoning About Knowledge. MIT Press, 1996.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computation Logic, 2(1), January 2001.","DOI":"10.1145\/371282.371311"},{"key":"7_CR8","unstructured":"M. Fisher. A resolution method for temporal logic. In Proc. 12th Int. Joint Conf. on Artificial Intelligence (IJCAI). Morgan Kaufman, 1991."},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1017\/S0269888900007670","volume":"11","author":"M. Fisher","year":"1996","unstructured":"M. Fisher. An introduction to executable temporal logics. Knowledge Engineering Review, 11:43\u201356, 1996.","journal-title":"Knowledge Engineering Review"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann. The Model Checker Spin. IEEE Trans. on Software Engineering, 23(5):279\u2013295, May 1997. Special Issue on Formal Methods in Software Practice.","DOI":"10.1109\/32.588521"},{"key":"7_CR11","unstructured":"U. Hustadt and R. Schmidt. Scientific Benchmarking with Temporal Logic Decision Procedures Proc. Int. Conf. on Principles of Knowledge Representation & Reasoning, 2002."},{"key":"7_CR12","unstructured":"U. Hustadt and R. Schmidt. Formulae which Highlight Differences between Temporal Logic and Dynamic Logic Provers In Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics, Italy, 2001."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"O. Kupferman and M. Vardi. Synthesis with incomplete informatio. In Advances in Temporal Logic. pp. 109\u2013128. Kluwer, 2000.","DOI":"10.1007\/978-94-015-9586-5_6"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. Princip. Prog. Lang., pp. 179\u2013190, 1989.","DOI":"10.1145\/75277.75293"},{"issue":"3","key":"7_CR16","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1093\/logcom\/8.3.293","volume":"8","author":"A. S. Rao","year":"1998","unstructured":"A. S. Rao and M. P. Georgeff. Decision procedures for BDI logics. Journal of Logic and Computation, 8(3):293\u2013342, 1998.","journal-title":"Journal of Logic and Computation"},{"key":"7_CR17","unstructured":"M. P. Shanahan. Solving the Frame Problem. MIT Press, 1997."},{"key":"7_CR18","unstructured":"A. Tansel, editor. Temporal Databases: theory, design, and implementation. Benjamin\/Cummings, 1993."},{"key":"7_CR19","unstructured":"G. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, 1968."},{"key":"7_CR20","first-page":"379","volume-title":"Frontiers of Combining Systems II","author":"F. Wolter","year":"2000","unstructured":"F. Wolter and M. Zakharyaschev. Temporalizing description logics. In Frontiers of Combining Systems II, pp. 379\u2013401. Research Studies Press LTD, England, 2000."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45616-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T11:08:17Z","timestamp":1737025697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}