Proof Search in Hajek's Basic Logic
<|reference_start|>Proof Search in Hajek's Basic Logic: 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.<|reference_end|>
@article{bova2006proof,
    title={Proof Search in Hajek's Basic Logic},
    author={S. Bova (1) and F. Montagna (1) ((1) University of Siena, Italy)},
    journal={arXiv preprint arXiv:cs/0605094},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0605094},
    primaryClass={cs.LO cs.CC}
}