Proof search and co-NP completeness for many-valued logics (Q1697337)

This paper generalizes relational hypersequents (as introduced in [the second author et al., Lect. Notes Comput. Sci. 3452, 496--510 (2005; Zbl 1109.03019)]) to disjunctions of arbitrary semantic predicates over multisets of formules. The authors introduce a methodology to define relational hypersequent calculi for a large class of many-valued logics and identify sufficient conditions on these calculi that guarantee the co-NP completeness of the logics. The methodology applies to projective and semi-projective logics as well as to Łukasiewicz logic, product logic and Hájek's basic fuzzy logic BL. It provides a unified perspective on most of the known complexity results for many valued logics. As the authors claim, this article subsumes all existing results on sequents of relations and relational hypersequent calculi found in [\textit{M. Baaz} and \textit{C. G. Fermüller}, Lect. Notes Comput. Sci. 1617, 36--50 (1999; Zbl 0931.03066); \textit{M. Baaz} et al., in: Beyond two: Theory and applications of multiple-valued logic. Heidelberg: Physica-Verlag. 157--180 (2003; Zbl 1041.03020); the second and the third author, Theor. Comput. Sci. 480, 26--42 (2013; Zbl 1322.03019); the second author et al., loc. cit.; \textit{T. Vetterlein}, J. Log. Comput. 18, No. 1, 35--57 (2008; Zbl 1139.03018); \textit{S. Bova} and the third author, ACM Trans. Comput. Log. 9, No. 3, Article No. 21, 26 p. (2008; Zbl 1367.03024)].