zbMATH — the first resource for mathematics

Polynomial space hardness without disjunction property. (English) Zbl 1298.68097
The present paper is a study of polynomial space hardness (PSPACE-hard) on all varieties in the interval between Heyting algebras with weak excluded middle (i.e., \(\lnot \alpha \vee \lnot \lnot \alpha \)) and divisible commutative integral residuated lattices. (This interval is referred to by H/CIR in this review.) In [R. Horčík and K. Terui, Theor. Comput. Sci. 412, No. 31, 3992–4006 (2011; Zbl 1231.03021)], it is shown that if a variety of residuated lattices has the disjunctive property (DP), then it has a PSPACE-hard equational theory. (The DP reads as follows: If \(\alpha \vee \beta \) is logically provable, then at least one of \(\alpha \) and \(\beta \) is logically provable as well.) Therefore, notice that all varieties with DP in H/CIR have a PSPACE-hard equational theory. In the paper under review, this result is extended by proving that all varieties in H/CIR have a PSPACE-hard equational theory, whence it follows that there are uncountably many varieties of residuated lattices lacking the DP and having a PSPACE-hard equational theory. The authors extend the idea of Statman’s reduction [R. Statman, Theor. Comput. Sci. 9, 67–72 (1979; Zbl 0411.03049)], which is essentially that “a decision algorithm for intuitionistic tautologies can simulate effectively a brute force decision algorithm for the quantified Boolean sentences” (p. 6). In particular, they show that Statman’s reduction only requires a special case of DP (i.e., it does not require the full DP). Finally, it is to be noted that the authors’ reduction only uses lattice and residual operations (multiplications and negations are not used).

68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03B70 Logic in computer science
03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03G25 Other algebras related to logic
08A70 Applications of universal algebra in computer science
Full Text: DOI