{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:53:49Z","timestamp":1715061229911},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2006,12,2]],"date-time":"2006-12-02T00:00:00Z","timestamp":1165017600000},"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":[[2007,2,28]]},"DOI":"10.1007\/s10817-006-9051-0","type":"journal-article","created":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T06:51:14Z","timestamp":1164955874000},"page":"173-199","source":"Crossref","is-referenced-by-count":29,"title":["An Optimal Decision Procedure for Right Propositional Neighborhood Logic"],"prefix":"10.1007","volume":"38","author":[{"given":"Davide","family":"Bresolin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guido","family":"Sciavicco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,12,2]]},"reference":[{"key":"9051_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem, Perspectives of Mathematical Logic","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem, Perspectives of Mathematical Logic. Springer, Berlin Heidelberg New York (1997)"},{"issue":"2","key":"9051_CR2","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1093\/logcom\/13.2.195","volume":"13","author":"H. Bowman","year":"2003","unstructured":"Bowman, H., Thompson, S.: A decision procedure and complete axiomatization of finite interval temporal logic with projection. J. Log. Comput. 13(2), 195\u2013239 (2003)","journal-title":"J. Log. Comput."},{"key":"9051_CR3","unstructured":"Bresolin, D., Montanari, A.: A tableau-based decision procedure for a branching-time interval temporal logic. In: Schlingloff, H. (ed.): Proceedings of the 4th International Workshop on Methods for Modalities, pp. 38\u201353. Berlin, Germany (2005a)"},{"key":"9051_CR4","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Montanari, A.: A tableau-based decision procedure for Right Propositional Neighborhood Logic. In: Proceedings of TABLEAUX 2005. Lecture Notes in Artificial Intelligence, vol. 3702, pp. 63\u201377. Koblenz, Germany (2005b)","DOI":"10.1007\/11554554_7"},{"key":"9051_CR5","doi-asserted-by":"crossref","unstructured":"Bresolin, D., Montanari, A.: A tableau-based decision procedure for right propositional neighborhood logic. Technical Report\u00a002, Dipartimento di Matematica e Informatica, Universit\u00e0 di Udine, Italy (2005c)","DOI":"10.1007\/11554554_7"},{"issue":"1","key":"9051_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E. Emerson","year":"1985","unstructured":"Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"9051_CR7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E. Emerson","year":"1984","unstructured":"Emerson, E., Sistla, A.: Deciding full branching time logic. Inf. Control 61(3), 175\u2013201 (1984)","journal-title":"Inf. Control"},{"key":"9051_CR8","doi-asserted-by":"crossref","unstructured":"Goranko, V., Montanari, A., Sciavicco, G.: A general tableau method for propositional interval temporal logic. In: Proceedings of TABLEAUX 2003. Lecture Notes in Artificial Intelligence, vol. 2796, pp. 102\u2013116. Rome, Italy (2003a)","DOI":"10.1007\/978-3-540-45206-5_10"},{"issue":"9","key":"9051_CR9","first-page":"1137","volume":"9","author":"V. Goranko","year":"2003","unstructured":"Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood temporal logics. J. Univers. Comput. Sci. 9(9), 1137\u20131167 (2003b)","journal-title":"J. Univers. Comput. Sci."},{"issue":"1\u20132","key":"9051_CR10","doi-asserted-by":"crossref","first-page":"9","DOI":"10.3166\/jancl.14.9-54","volume":"14","author":"V. Goranko","year":"2004","unstructured":"Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. J. Appl. Non-class. Log. 14(1\u20132), 9\u201354 (2004)","journal-title":"J. Appl. Non-class. Log."},{"issue":"3","key":"9051_CR11","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/j.jal.2005.06.012","volume":"4","author":"V. Goranko","year":"2006","unstructured":"Goranko, V., Montanari, A., Sciavicco, G., Sala, P.: A general tableau method for propositional interval temporal logics: theory and implementation. J. Appl. Logic 4(3), 305\u2013330 (2006)","journal-title":"J. Appl. Logic"},{"issue":"4","key":"9051_CR12","first-page":"935","volume":"38","author":"J. Halpern","year":"1991","unstructured":"Halpern, J., Shoham, Y.: A propositional modal logic of time intervals. ACM 38(4), 935\u2013962 (1991)","journal-title":"ACM"},{"key":"9051_CR13","first-page":"97","volume-title":"Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece. Lecture Notes in Computer Science, vol. 697","author":"Y. Kesten","year":"1993","unstructured":"Kesten, Y., Manna, Z., McGuire, H., Pnueli, A.: A decision algorithm for full propositional temporal logic. In: Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece. Lecture Notes in Computer Science, vol. 697, vol. 697, pp. 97\u2013109. Springer, Berlin Heidelberg New York (1993)"},{"key":"9051_CR14","first-page":"290","volume-title":"Proceedings of 6th Asian Computing Science Conference. Lecture Notes in Computer Science, vol. 1961","author":"K. Lodaya","year":"2000","unstructured":"Lodaya, K.: Sharpening the undecidability of interval temporal logic. In: Proceedings of 6th Asian Computing Science Conference. Lecture Notes in Computer Science, vol. 1961, pp. 290\u2013298. Springer, Berlin Heidelberg New York (2000)"},{"key":"9051_CR15","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1109\/TIME.2005.30","volume-title":"Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME), Burlington, VT","author":"A. Montanari","year":"2005","unstructured":"Montanari, A.: Propositional interval temporal logics: some promising paths. In: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME), Burlington, VT, pp. 201\u2013203. IEEE Computer Society Press, Los Alamitos, CA (2005)"},{"key":"9051_CR16","unstructured":"Montanari, A., Sciavicco, G.: A Decidability Proof for Propositional Neighborhood Logic (Extended Abstract). Contributed Talk, Trends in Logics III Conference, Warsaw - Ruciane Nida (Poland) (2005)"},{"key":"9051_CR17","first-page":"259","volume-title":"Proceedings of the 8th European Conference on Logics in Artificial Intelligence, Cosenza, Italy. Lecture Notes in Artificial Intelligence, vol. 2424","author":"A. Montanari","year":"2002","unstructured":"Montanari, A., Sciavicco, G., Vitacolonna, N.: Decidability of interval temporal logics over split-frames via granularity. In: Proceedings of the 8th European Conference on Logics in Artificial Intelligence, Cosenza, Italy. Lecture Notes in Artificial Intelligence, vol. 2424, pp. 259\u2013270. Springer, Berlin Heidelberg New York (2002)"},{"key":"9051_CR18","unstructured":"Moszkowski, B.: Reasoning about digital circuits. Technical report stan-cs-83-970, Department of Computer Science, Stanford University, Stanford, CA (1983)"},{"issue":"2","key":"9051_CR19","doi-asserted-by":"crossref","first-page":"685","DOI":"10.2307\/2695037","volume":"66","author":"M. Otto","year":"2001","unstructured":"Otto, M.: Two variable first-order logic over ordered domains. J. Symb. Log. 66(2), 685\u2013702 (2001)","journal-title":"J. Symb. Log."},{"key":"9051_CR20","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/BFb0035385","volume-title":"3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Enschede, The Netherlands. Lecture Notes in Computer Science, vol. 1217","author":"P. Schmitt","year":"1997","unstructured":"Schmitt, P., Goubault-Larrecq, J.: A tableau system for linear-time temporal togic. In: Brinksma, E. (ed.) 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Enschede, The Netherlands. Lecture Notes in Computer Science, vol. 1217, pp. 130\u2013144. Springer, Berlin Heidelberg New York (1997)"},{"issue":"4","key":"9051_CR21","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1093\/logcom\/1.4.453","volume":"1","author":"Y. Venema","year":"1991","unstructured":"Venema, Y.: A modal logic for chopping intervals. J. Log. Comput. 1(4), 453\u2013476 (1991)","journal-title":"J. Log. Comput."},{"key":"9051_CR22","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Log. Anal. 28, 119\u2013136 (1985)","journal-title":"Log. Anal."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9051-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9051-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9051-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:47Z","timestamp":1559251307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9051-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12,2]]},"references-count":22,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2007,2,28]]}},"alternative-id":["9051"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9051-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,2]]}}}