{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T21:51:30Z","timestamp":1778277090286,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755586","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_5","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T05:36:46Z","timestamp":1191649006000},"page":"32-46","source":"Crossref","is-referenced-by-count":8,"title":["One-Pass Tableaux for Computation Tree Logic"],"prefix":"10.1007","author":[{"given":"Pietro","family":"Abate","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Widmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Abate, P.: The Tableau Workbench: a framework for building automated tableau-based theorem provers. PhD thesis, The Australian National University (2006)"},{"key":"5_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-45744-5_8","volume-title":"Automated Reasoning","author":"F. Baader","year":"2001","unstructured":"Baader, F., Tobies, S.: The inverse method implements the automata approach for modal satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 92\u2013106. Springer, Heidelberg (2001)"},{"key":"5_CR3","unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: an alternative to terminological cycles. Technical Report, DFKI (1990)"},{"issue":"3","key":"5_CR4","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10472-006-9018-1","volume":"46","author":"A. Basukoski","year":"2006","unstructured":"Basukoski, A., Bolotov, A.: A clausal resolution method for branching time logic ECTL+. Annals of Mathematics and Artificial Intelligence\u00a046(3), 235\u2013263 (2006)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: Proceedings of Principles of Programming Languages (1981)","DOI":"10.1145\/567532.567551"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. of Computer and System Sci.\u00a030, 1\u201324 (1985)","journal-title":"J. of Computer and System Sci."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic (2001)","DOI":"10.1145\/371282.371311"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., Orejas, F.: A Cut-Free and Invariant-Free Sequent Calculus for PLTL. In: 6th EACSL Annual Conference on Computer Science and Logic (to appear, 2007)","DOI":"10.1007\/978-3-540-74915-8_36"},{"key":"5_CR9","unstructured":"Gough, G.: Decision procedures for temporal logics. Master\u2019s thesis, Dept. of Computer Science, University of Manchester, England (1984)"},{"key":"5_CR10","volume-title":"Model checking","author":"O. Grumberg","year":"1999","unstructured":"Grumberg, O., Clarke, E.M., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Patel-Schneider, P.F.: Optimising description logic subsumption. Journal of Logic and Computation\u00a09(3), 267\u2013293 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"5_CR12","unstructured":"Horrocks, I., Sattler, U.: A tableaux decision procedure for SHOIQ. In: Proc. of the 19th Int. Joint Conf. on Artificial Intelligence, pp. 448\u2013453 (2005)"},{"key":"5_CR13","unstructured":"Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Collegium Logicum, Kurt G\u00f6del Society, pp. 65\u201379 (2004)"},{"issue":"1-3","key":"5_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.apal.2004.10.004","volume":"133","author":"G. J\u00e4ger","year":"2005","unstructured":"J\u00e4ger, G., Alberucci, L.: About cut elimination for logics of common knowledge. Ann. Pure Appl. Logic\u00a0133(1-3), 73\u201399 (2005)","journal-title":"Ann. Pure Appl. Logic"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"J\u00e4ger, G., Kretz, M., Studer, T.: Cut-free common knowledge. Journal of Applied Logic (to appear)","DOI":"10.1016\/j.jal.2006.02.003"},{"key":"5_CR16","unstructured":"Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis, Eindhoven University of Technology, The Netherlands (1999)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 97\u2013109. Springer, Heidelberg (1993)"},{"key":"5_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/11590156_31","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"M. Reynolds","year":"2005","unstructured":"Reynolds, M.: Towards a CTL* tableau. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 384\u2013395. Springer, Heidelberg (2005)"},{"key":"5_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 277\u2013291. Springer, Heidelberg (1998)"},{"issue":"1-2","key":"5_CR21","doi-asserted-by":"publisher","first-page":"169","DOI":"10.3166\/jancl.16.169-207","volume":"16","author":"M.Y. Vardi","year":"2006","unstructured":"Vardi, M.Y., Pan, G., Sattler, U.: BDD-based decision procedures for K. Journal of Applied Non-Classical Logics\u00a016(1-2), 169\u2013208 (2006)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer Systems and Science (1986)","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Trans. on Comp. Logic\u00a02(2) (2001)","DOI":"10.1145\/371316.371511"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. and Cont.\u00a056, 72\u201399 (1983)","journal-title":"Inf. and Cont."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:48Z","timestamp":1619519088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_5","relation":{},"subject":[]}}