Polynomial space hardness without disjunction property
type: Item
instance of: scholarly article
title: Polynomial space hardness without disjunction property
zbMATH Open document ID: 1298.68097
author: Simone Bova
author: Franco Montagna
published in: Theoretical Computer Science
publication date: 2013-02-19T00:00:00Z
review text: 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 [\textit{R. Horčík} and \textit{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 \textit{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 [\textit{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).
reviewed by: Gemma Robles
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03G25
Mathematics Subject Classification ID: 08A70
zbMATH DE Number: 6137325
zbMATH Keywords: substructural logics
zbMATH Keywords: computational complexity
MaRDI profile type: Publication
full work available at URL: j.tcs.2012.08.025
OpenAlex ID: W1986786317
DOI: 10.1016/J.TCS.2012.08.025
Recommended article: Partial algebras and complexity of satisfiability and universal theory for distributive lattices, Boolean algebras and Heyting algebras
Recommended article: On the Complexity of the Equational Theory of Residuated Boolean Algebras
Recommended article: Free-decomposability in varieties of pseudocomplemented residuated lattices
Recommended article: Compatible operations on residuated lattices
Recommended article: Generalized ordinal sums and translations
Recommended article: Splittings in varieties of logic
Recommended article: Computational complexity of the word problem in modal and Heyting algebras with a small number of generators
Recommended article: A note on the complexity of propositional Hoare logic
Recommended article: Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
Recommended article: Lattice embeddings for abstract bounded reducibilities
description: scientific article; zbMATH DE number 6137325