{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:41:02Z","timestamp":1649155262869},"reference-count":9,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,6]]},"abstract":"\n We introduce a proof system for H\u00e1jek's logic\n BL<\/jats:bold>\n based on a relational hypersequents framework. We prove that the rules of our logical calculus, called\n RHBL<\/jats:bold>\n , are sound and invertible with respect to any valuation of\n BL<\/jats:bold>\n into a suitable algebra, called (\u03c9)[0,1]. Refining the notion of reduction tree that arises naturally from\n RHBL<\/jats:bold>\n , we obtain a decision algorithm for\n BL<\/jats:bold>\n provability whose running time upper bound is 2\n \n O<\/jats:italic>\n (\n n<\/jats:italic>\n )\n <\/jats:sup>\n , where\n 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 O<\/jats:italic>\n (\n n<\/jats:italic>\n 3<\/jats:sup>\n ), we can describe a polynomial time verification algorithm for\n 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","source":"Crossref","is-referenced-by-count":6,"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"}]},{"given":"Franco","family":"Montagna","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Siena, Siena, Italy"}]}],"member":"320","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","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."},{"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","doi-asserted-by":"crossref","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.","DOI":"10.1007\/978-94-011-5300-3"},{"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","unstructured":"Schrijver A. 1986. Theory of Linear and Integer Programming. John Wiley & Sons Ltd. Chichester U.K. Schrijver A. 1986. Theory of Linear and Integer Programming. John Wiley & Sons Ltd. Chichester U.K."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1352582.1352589","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,20]],"date-time":"2021-02-20T03:39:19Z","timestamp":1613792359000},"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":"http:\/\/dx.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":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2008,6]]}}}