Proof search in Hájek's basic logic

ABSTRACT

We introduce a proof system for Hájek'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 (ω)[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 (ω)[0, 1]. Finally, since the size of the reduction tree branches is O(n³), we can describe a polynomial time verification algorithm for BL unprovability.

REFERENCES

• 1: Uniform Description of Calculi for All t-Norm Logics, Proceedings of the 34th International Symposium on Multiple-Valued Logic, p.38-43, May 19-22, 2004
• 2: Baaz, M., Hájek, P., Montagna, F., and Veith, H. 2002. Complexity of t-tautologies. Ann. Pure Appl. Logic 113, 1-3, 3--11.
• 3: Ciabattoni, A., Fermüller, 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.
• 4: Cignoli, R., Esteva, F., Godo, L., and Torrens, A. 2000. Basic fuzzy logic is the logic of continuous t-norms and their residua. Soft Comput. 4, 2, 106--112.
• 5: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 6: Hájek, P. 1998. Metamathematics of Fuzzy Logic. Kluwer Academic Publishers, Dordrecht, The Netherlands.
• 7: Montagna, F., Pinna, G. M., and Tiezzi, E. B. P. 2003. A tableau calculus for Hájek's logic BL. J. Logic Comput. 13, 2, 241--259.
• 8: D. Mundici, Satisfiability in many-valued sentential logic is NP-complete, Theoretical Computer Science, v.52 n.1-2, p.145-153, May 1987 [doi>10.1016/0304-3975(87)90083-1]
• 9: Alexander Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic; Mechanical theorem proving; Proof theory
      F.4.3 Formal Languages
          Subjects: Decision problems

General Terms:
Algorithms, Theory

Keywords:
Fuzzy logic, automated deduction, countermodel building