{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,6]],"date-time":"2024-08-06T02:03:06Z","timestamp":1722909786271},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,12,2]],"date-time":"2011-12-02T00:00:00Z","timestamp":1322784000000},"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":[[2013,1]]},"DOI":"10.1007\/s10817-011-9241-2","type":"journal-article","created":{"date-parts":[[2011,12,3]],"date-time":"2011-12-03T06:46:53Z","timestamp":1322894813000},"page":"1-49","source":"Crossref","is-referenced-by-count":3,"title":["Invariant-Free Clausal Temporal Resolution"],"prefix":"10.1007","volume":"50","author":[{"given":"Jose","family":"Gaintzarain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Montserrat","family":"Hermo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paqui","family":"Lucio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa","family":"Navarro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fernando","family":"Orejas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,12,2]]},"reference":[{"key":"9241_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Manna, Z.: Nonclausal temporal deduction. In: Parikh, R. (ed.) Logic of Programs, vol.\u00a0193 of Lecture Notes in Computer Science, pp.\u00a01\u201315. Springer (1985)","DOI":"10.1007\/3-540-15648-8_1"},{"issue":"2","key":"9241_CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M Abadi","year":"1990","unstructured":"Abadi, M., Manna, Z.: Nonclausal deduction in first-order temporal logic. J. ACM 37(2), 279\u2013317 (1990)","journal-title":"J. ACM"},{"key":"9241_CR3","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/978-3-540-75560-9_5","volume-title":"Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR\u201907","author":"P Abate","year":"2007","unstructured":"Abate, P., Gor\u00e9, R., Widmann, F.: One-pass tableaux for computation tree logic. In: Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR\u201907, pp.\u00a032\u201346. Springer-Verlag, Berlin (2007)"},{"key":"9241_CR4","doi-asserted-by":"crossref","unstructured":"Banieqbal, B., Barringer, H.: Temporal logic with fixed points. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Proceedings Temporal Logic in Specification, Altrincham, UK, vol.\u00a0398 of Lecture Notes in Computer Science, pp.\u00a062\u201374. Springer, 8\u201310 April 1987","DOI":"10.1007\/3-540-51803-7_22"},{"key":"9241_CR5","doi-asserted-by":"crossref","unstructured":"Baudinet, M.: Temporal logic programming is complete and expressive. In: Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL), pp.\u00a0267\u2013280. Austin, Texas (1989)","DOI":"10.1145\/75277.75301"},{"issue":"1","key":"9241_CR6","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1080\/095281399146625","volume":"11","author":"A Bolotov","year":"1999","unstructured":"Bolotov, A., Fisher, M.: A clausal resolution method for CTL branching-time temporal logic. J. Exp. Theor. Artif. Intell. 11(1), 77\u201393 (1999)","journal-title":"J. Exp. Theor. Artif. Intell."},{"issue":"2","key":"9241_CR7","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1145\/639624.802066","volume":"14","author":"AR Cavalli","year":"1984","unstructured":"Cavalli, A.R.: A method of automatic proof for the specification and verification of protocols. Comput. Commun. Rev. 14(2), 100\u2013106 (1984)","journal-title":"Comput. Commun. Rev."},{"key":"9241_CR8","series-title":"Lecture Notes in Computer Science","first-page":"113","volume-title":"Proceedings on 7th International Conference on Automated Deduction","author":"AR Cavalli","year":"1984","unstructured":"Cavalli, A.R., del Cerro, L.F.: A decision method for linear temporal logic. In: Shostak, R.E. (ed.) Proceedings on 7th International Conference on Automated Deduction, vol.\u00a0170 of Lecture Notes in Computer Science, pp.\u00a0113\u2013127. Springer, Napa, California, 14\u201316 May 1984"},{"key":"9241_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-45616-3_7","volume-title":"Proceedings on Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002","author":"A Degtyarev","year":"2002","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: Proceedings on Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, vol.\u00a02381 of Lecture Notes in Computer Science, pp.\u00a085\u201399. Springer, Copenhagen, 30 July\u20131 August 2002"},{"key":"9241_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1007\/3-540-61511-3_121","volume-title":"Proceedings on Automated Deduction\u2014CADE-13, 13th International Conference on Automated Deduction","author":"C Dixon","year":"1996","unstructured":"Dixon, C.: Search strategies for resolution in temporal logics. In: McRobbie, M.A., Slaney, J.K. (eds.) Proceedings on Automated Deduction\u2014CADE-13, 13th International Conference on Automated Deduction, vol.\u00a01104 of Lecture Notes in Computer Science, pp.\u00a0673\u2013687. Springer, New\u00a0Brunswick, 30 July\u20133 August 1996"},{"key":"9241_CR11","doi-asserted-by":"crossref","unstructured":"Eder, E.: Relative complexities of first-order calculi. Artif. Intell. Vieweg (1992)","DOI":"10.1007\/978-3-322-84222-0"},{"key":"9241_CR12","unstructured":"Fisher, M.: A resolution method for temporal logic. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI), pp.\u00a099\u2013104. Sydney, Australia (1991)"},{"key":"9241_CR13","doi-asserted-by":"crossref","unstructured":"Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. John Wiley & Sons, Ltd (2011)","DOI":"10.1002\/9781119991472"},{"issue":"1","key":"9241_CR14","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Log. 2(1), 12\u201356 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"9241_CR15","volume-title":"Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1","year":"1994","unstructured":"Gabbay, D.M., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, Inc., New York (1994)"},{"key":"9241_CR16","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537687.001.0001","volume-title":"Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 2","author":"DM Gabbay","year":"2000","unstructured":"Gabbay, D.M., Reynolds, M.A., Finger, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 2. Oxford University Press, Inc., New York (2000)"},{"key":"9241_CR17","doi-asserted-by":"crossref","unstructured":"Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M.: Systematic semantic tableaux for PLTL. In: Pimentel, E. (ed.) Proceedings of the 7th Spanish Conference on Programming and Computer Languages (PROLE 2007), Selected Papers, vol.\u00a0206 of Electronic Notes in Theoretical Computer Science, pp.\u00a059\u201373 (2008)","DOI":"10.1016\/j.entcs.2008.03.075"},{"key":"9241_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-540-74915-8_36","volume-title":"Proceedings on Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL","author":"J Gaintzarain","year":"2007","unstructured":"Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., Orejas, F.: A cut-free and invariant-free sequent calculus for PLTL. In: Duparc, J., Henzinger, T.A. (eds.) Proceedings on Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, vol.\u00a04646 of Lecture Notes in Computer Science, pp.\u00a0481\u2013495. Springer, Lausanne, 11\u201315 September 2007"},{"issue":"8","key":"9241_CR19","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1016\/j.jlap.2009.05.001","volume":"78","author":"J Gaintzarain","year":"2009","unstructured":"Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., Orejas, F.: Dual systems of tableaux and sequents for PLTL. Journal of Logic and Algebraic Programming 78(8), 701\u2013722 (2009)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9241_CR20","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/j.entcs.2010.04.009","volume":"262","author":"V Goranko","year":"2010","unstructured":"Goranko, V., Kyrilov, A., Shkatov, D.: Tableau tool for testing satisfiability in LTL: implementation and experimental analysis. Electr. Notes Theor. Comput. Sci. 262, 113\u2013125 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9241_CR21","unstructured":"Goranko, V., Shkatov, D.: Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time. In: Proceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems, AAMAS \u201909, pp.\u00a0969\u2013976, vol.\u00a02. Richland, SC, International Foundation for Autonomous Agents and Multiagent Systems (2009)"},{"key":"9241_CR22","doi-asserted-by":"crossref","unstructured":"Gore, R.: Tableau Methods for Modal and Temporal Logics, pp.\u00a0297\u2013396. Kluwer Academic Publishers (1999)","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"9241_CR23","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/978-3-642-02959-2_32","volume-title":"Proceedings of the 22nd International Conference on Automated Deduction, CADE-22","author":"R Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: An optimal on-the-fly tableau-based decision procedure for pdl-satisfiability. In: Proceedings of the 22nd International Conference on Automated Deduction, CADE-22, pp.\u00a0437\u2013452. Springer-Verlag, Berlin (2009)"},{"key":"9241_CR24","unstructured":"Gough, G.D.: Decision Procedures for Temporal Logic. Master\u2019s thesis. Department of Computer Science, University of Manchester, England (1984)"},{"key":"9241_CR25","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Konev, B.: Trp+\u2009+2.0: A temporal resolution prover. In: Baader, F. (ed.) Proceedings on Automated Deduction\u2014CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, vol.\u00a02741 of Lecture Notes in Computer Science, pp.\u00a0274\u2013278. Springer, 28 July\u20132 August 2003","DOI":"10.1007\/978-3-540-45085-6_21"},{"issue":"4","key":"9241_CR26","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/11663081.1999.10510981","volume":"9","author":"U Hustadt","year":"1999","unstructured":"Hustadt, U., Schmidt, R.A.: An empirical analysis of modal theorem provers. J. Appl. Non-class. Log. 9(4), 479\u2013522 (1999)","journal-title":"J. Appl. Non-class. Log."},{"key":"9241_CR27","unstructured":"Janssen, G.: Logics for digital circuit verification\u2014theory, algorithms and applications. PhD thesis, Eindhoven University of Technology, The Netherland (1999)"},{"issue":"1","key":"9241_CR28","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/B:STUD.0000027468.28935.6d","volume":"76","author":"R Kontchakov","year":"2004","unstructured":"Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporalising tableaux. Stud. Log. 76(1), 91\u2013134 (2004)","journal-title":"Stud. Log."},{"issue":"1","key":"9241_CR29","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Log. J. IGPL 8(1), 55\u201385 (2000)","journal-title":"Log. J. IGPL"},{"key":"9241_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/978-3-642-05089-3_26","volume-title":"Proceedings on FM 2009: Formal Methods, 2nd World Congress","author":"M Reynolds","year":"2009","unstructured":"Reynolds, M.: A tableau for ctl. In: Proceedings on FM 2009: Formal Methods, 2nd World Congress, vol.\u00a05850 of Lecture Notes in Computer Science, pp.\u00a0403\u2013418. Springer Eindhoven, The Netherlands, 2\u20136 November 2009"},{"key":"9241_CR31","doi-asserted-by":"crossref","unstructured":"Reynolds, M., Dixon, C.: Theorem-proving for discrete temporal logic. In: Handbook of Temporal Reasoning in Artificial Intelligence, pp.\u00a0279\u2013314. Elsevier (2005)","DOI":"10.1016\/S1574-6526(05)80011-2"},{"key":"9241_CR32","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9241_CR33","volume-title":"Logic for Computer Scientists","author":"U Sch\u00f6ning","year":"1989","unstructured":"Sch\u00f6ning, U.: Logic for Computer Scientists. Birkh\u00e4user, Boston-Basel-Berlin (1989)"},{"key":"9241_CR34","doi-asserted-by":"crossref","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: Analytic Tableaux and Related Methods, vol.\u00a01397 of Lecture Notes in Computer Science, pp.\u00a0277\u2013292 (1998)","DOI":"10.1007\/3-540-69778-0_28"},{"key":"9241_CR35","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"AP Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for b\u00fcchi automata with applications to temporal logic. Theor. Comput. Sci. 49, 217\u2013237 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"9241_CR36","series-title":"Lecture Notes in Computer Science","first-page":"16","volume-title":"Proceedings on 5th Conference Foundations of Software Technology and Theoretical Computer Science","author":"G Venkatesh","year":"1985","unstructured":"Venkatesh, G.: A decision method for temporal logic based on resolution. In: Maheshwari, S.N. (ed.) Proceedings on 5th Conference Foundations of Software Technology and Theoretical Computer Science, vol.\u00a0206 of Lecture Notes in Computer Science, pp.\u00a0272\u2013289. Springer, New\u00a0Delhi, India, 16\u201318 December 1985"},{"issue":"1\u20132","key":"9241_CR37","doi-asserted-by":"crossref","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. Control 56(1\u20132), 72\u201399 (1983)","journal-title":"Inf. Control"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9241-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9241-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9241-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,15]],"date-time":"2024-04-15T06:33:16Z","timestamp":1713162796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9241-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,2]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,1]]}},"alternative-id":["9241"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9241-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,2]]}}}