{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T09:38:54Z","timestamp":1778578734849,"version":"3.51.4"},"reference-count":9,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,6,1]],"date-time":"2008-06-01T00:00:00Z","timestamp":1212278400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:p>\n            We introduce a proof system for H\u00e1jek's logic\n            <jats:bold>BL<\/jats:bold>\n            based on a relational hypersequents framework. We prove that the rules of our logical calculus, called\n            <jats:bold>RHBL<\/jats:bold>\n            , are sound and invertible with respect to any valuation of\n            <jats:bold>BL<\/jats:bold>\n            into a suitable algebra, called (\u03c9)[0,1]. Refining the notion of reduction tree that arises naturally from\n            <jats:bold>RHBL<\/jats:bold>\n            , we obtain a decision algorithm for\n            <jats:bold>BL<\/jats:bold>\n            provability whose running time upper bound is 2\n            <jats:sup>\n              <jats:italic>O<\/jats:italic>\n              (\n              <jats:italic>n<\/jats:italic>\n              )\n            <\/jats:sup>\n            , where\n            <jats:italic>n<\/jats:italic>\n            is the number of connectives of the input formula. Moreover, if a formula is unprovable, we exploit the constructiveness of a polynomial time algorithm for leaves validity for providing a procedure to build countermodels in (\u03c9)[0, 1]. Finally, since the size of the reduction tree branches is\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>3<\/jats:sup>\n            ), we can describe a polynomial time verification algorithm for\n            <jats:bold>BL<\/jats:bold>\n            unprovability.\n          <\/jats:p>","DOI":"10.1145\/1352582.1352589","type":"journal-article","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T13:30:05Z","timestamp":1213104605000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Proof search in H\u00e1jek's basic logic"],"prefix":"10.1145","volume":"9","author":[{"given":"Simone","family":"Bova","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Siena, Siena, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Montagna","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Siena, Siena, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,6,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/998681.1006795"},{"key":"e_1_2_1_2_1","first-page":"1","article-title":"Complexity of t-tautologies","volume":"113","author":"Baaz M.","year":"2002","unstructured":"Baaz , M. , H\u00e1jek , P. , Montagna , F. , and Veith , H. 2002 . Complexity of t-tautologies . Ann. Pure Appl. Logic 113 , 1 - 3 , 3--11. Baaz, M., H\u00e1jek, P., Montagna, F., and Veith, H. 2002. Complexity of t-tautologies. Ann. Pure Appl. Logic 113, 1-3, 3--11.","journal-title":"Ann. Pure Appl. Logic"},{"key":"e_1_2_1_3_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"3452","author":"Ciabattoni A.","unstructured":"Ciabattoni , A. , Ferm\u00fcller , C. G. , and Metcalfe , G . 2004. Uniform rules and dialogue games for fuzzy logics. In Logic for Programming, Artificial Intelligence and Reasoning, F. Baader and A. Voronkov , Eds. Lecture Notes in Computer Science , vol. 3452 . Springer, Berlin, Germany, 496--510. Ciabattoni, A., Ferm\u00fcller, C. G., and Metcalfe, G. 2004. Uniform rules and dialogue games for fuzzy logics. In Logic for Programming, Artificial Intelligence and Reasoning, F. Baader and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 3452. Springer, Berlin, Germany, 496--510."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s005000000044"},{"key":"e_1_2_1_5_1","unstructured":"Cormen T. H. Leiserson C. E. Rivest R. L. and Stein C. 2001. Introduction to Algorithms 2nd ed. MIT Press Cambridge MA.   Cormen T. H. Leiserson C. E. Rivest R. L. and Stein C. 2001. Introduction to Algorithms 2nd ed. MIT Press Cambridge MA."},{"key":"e_1_2_1_6_1","volume-title":"Metamathematics of Fuzzy Logic","author":"H\u00e1jek P.","unstructured":"H\u00e1jek , P. 1998. Metamathematics of Fuzzy Logic . Kluwer Academic Publishers , Dordrecht, The Netherlands. H\u00e1jek, P. 1998. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, Dordrecht, The Netherlands."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.2.241"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90083-1"},{"key":"e_1_2_1_9_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver A.","unstructured":"Schrijver , A. 1986. Theory of Linear and Integer Programming . John Wiley &amp; Sons Ltd ., Chichester, U.K. Schrijver, A. 1986. Theory of Linear and Integer Programming. John Wiley &amp; Sons Ltd., Chichester, U.K."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1352582.1352589","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1352582.1352589","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:39:20Z","timestamp":1750253960000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1352582.1352589"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":9,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["10.1145\/1352582.1352589"],"URL":"https:\/\/doi.org\/10.1145\/1352582.1352589","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,6]]},"assertion":[{"value":"2006-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-06-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}