Proof Search in Hajek's Basic Logic
| dc.creator | Bova, S. | |
| dc.creator | Montagna, F. | |
| dc.date | 2006-05-22 | |
| dc.date.accessioned | 2026-07-07T07:09:33Z | |
| dc.date.available | 2026-07-07T07:09:33Z | |
| dc.description | We introduce a proof system for Hajek's logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL, are sound and invertible with respect to any valuation of BL into a suitable algebra, called omega[0,1]. Refining the notion of reduction tree that arises naturally from RHBL, we obtain a decision algorithm for BL provability whose running time upper bound is 2^O(n), where 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 omega[0,1]. Finally, since the size of the reduction tree branches is O(n^3), we can describe a polynomial time verification algorithm for BL unprovability. | |
| dc.description | 26 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0605094 | |
| dc.identifier | http://arxiv.org/abs/cs/0605094 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/111106 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | Computational Complexity | |
| dc.subject | F.4.1 | |
| dc.title | Proof Search in Hajek's Basic Logic | |
| dc.type | text |