{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T15:05:32Z","timestamp":1747580732943},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_6","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T09:36:30Z","timestamp":1167384990000},"page":"73-87","source":"Crossref","is-referenced-by-count":10,"title":["Normal Forms and Proofs in Combined Modal and Temporal Logics"],"prefix":"10.1007","author":[{"given":"U.","family":"Hustadt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1080\/11663081.1995.10510854","volume":"2","author":"F. Baader","year":"1995","unstructured":"Baader, F., Ohlbach, H.J.: A multi-dimensional terminological knowledge representation language. Journal of Applied Non-Classical Logics\u00a02, 153\u2013197 (1995)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"6_CR2","unstructured":"Bachmair, L., Ganzinger, H.: A theory of resolution. Research report MPII- 97-2-005, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany. To appear in Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (1997)"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1004991115882","volume":"59","author":"P. Blackburn","year":"1997","unstructured":"Blackburn, P., de Rijke, M.: Why combine logics? Studia Logica\u00a059, 5\u201327 (1997)","journal-title":"Studia Logica"},{"key":"6_CR4","unstructured":"de Nivelle, H.: Translation of S4 into GF and 2VAR. Manuscript (1999)"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1093\/logcom\/8.3.345","volume":"8","author":"C. Dixon","year":"1998","unstructured":"Dixon, C., Fisher, M., Wooldridge, M.: Resolution for temporal logics of knowledge. Journal of Logic and Computaton\u00a08(3), 345\u2013372 (1998)","journal-title":"Journal of Logic and Computaton"},{"key":"6_CR6","volume-title":"Reasoning About Knowledge","author":"R. Fagin","year":"1996","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1996)"},{"key":"6_CR7","unstructured":"Finger, M.: Notes on several methods for combining temporal logic systems. Presented at ESSLLI 1994 (1994)"},{"issue":"4","key":"6_CR8","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.2307\/2275807","volume":"61","author":"D.M. Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Fibred semantics and the weaving of logics. Part 1. Modal and intuitionistic logics. Journal of Symbolic Logic\u00a061(4), 1057\u20131120 (1996)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR9","unstructured":"Ghidini, C., Serafini, L.: Distributed first order logics. In: Gabbay, D.M., de Rijke, M. (eds.) Proc. FroCoS 1998 (1998) (to appear)"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/2.1.5","volume":"2","author":"V. Goranko","year":"1992","unstructured":"Goranko, V., Passy, S.: Using the universal modality: Gains and questions. Journal of Logic and Computation\u00a02(1), 5\u201330 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Using reasoning about knowledge to analyse distributed systems. Annual Review of Computer Science\u00a02 (1987)","DOI":"10.1146\/annurev.cs.02.060187.000345"},{"key":"#cr-split#-6_CR12.1","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Dixon, C., Schmidt, R., Fisher, M.: Normal forms and proofs in combined modal and temporal logics (2000);","DOI":"10.1007\/10720084_6"},{"key":"#cr-split#-6_CR12.2","unstructured":"Extended version of this paper, available at http:\/\/www.card.mmu.ac.uk\/U.Hustadt\/publications\/HDSF2000b.ps.gz"},{"key":"6_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/3-540-46508-1_13","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 192\u2013206. Springer, Heidelberg (2000)"},{"key":"6_CR14","first-page":"1429","volume-title":"Proc. IJCAI 1999","author":"N.R. Jennings","year":"1999","unstructured":"Jennings, N.R.: Agent-based computing: Promise and perils. In: Dean, T. (ed.) Proc. IJCAI 1999, pp. 1429\u20131436. Morgan Kaufmann, San Francisco (1999)"},{"key":"6_CR15","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1017\/CBO9780511600821.022","volume-title":"People and Computers IX","author":"C.W. Johnson","year":"1994","unstructured":"Johnson, C.W.: The formal analysis of human-computer interaction during accidents investigations. In: People and Computers IX, pp. 285\u2013300. Cambridge University Press, Cambridge (1994)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Ohlbach, H.J.: Combining Hilbert style and semantic reasoning in a resolution framework. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 205\u2013219. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0054261"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Ohlbach, H.J., Gabbay, D.M.: Calendar logic. Journal of Applied Non- Classical Logics\u00a08(4) (1998)","DOI":"10.1080\/11663081.1998.10510948"},{"key":"6_CR18","unstructured":"Wolter, F., Zakharyaschev, M.: Satisability problem in description logics with modal operators. In: Cohn, A.G., Schubert, L.K., Shapiro, S.C. (eds.) Proc. KR 1998, pp. 512\u2013523. Morgan Kaufmann, San Francisco (1998)"},{"issue":"3","key":"6_CR19","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1080\/11663081.1998.10510944","volume":"8","author":"M. Wooldridge","year":"1998","unstructured":"Wooldridge, M., Dixon, C., Fisher, M.: A tableau-based proof method for temporal logics of knowledge and belief. Journal of Applied Non-Classical Logics\u00a08(3), 225\u2013258 (1998)","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1017\/S0269888900008122","volume":"10","author":"M. Wooldridge","year":"1995","unstructured":"Wooldridge, M., Jennings, N.R.: Intelligent agents: Theory and practice. The Knowledge Engineering Review\u00a010(2), 115\u2013152 (1995)","journal-title":"The Knowledge Engineering Review"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:34:44Z","timestamp":1556004884000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/10720084_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}