Kanovich, M. I. Quasipolynomial algorithms for recognizing the satisfiability and derivability of propositional formulas. (English. Russian original) Zbl 0629.03013 Sov. Math., Dokl. 34, 273-277 (1987); translation from Dokl. Akad. Nauk SSSR 290, 281-286 (1986). Cases are considered where an exponential general problem can be broken up into subclasses of polynomial complexity. Quasipolynomiality is defined by \(O(| x|^{r(x)})\), where \(| x|\) is the length of the expression for the problem x, and r(x) is its rank. The paper proposes quasipolynomial algorithms to recognize the satisfiability of propositional formulas, and the derivability of formulas in the classical and intuitionistic propositional calculi. Free and flexible classes of implicative normal forms are introduced, too. Reviewer: E.Knuth Cited in 1 ReviewCited in 1 Document MSC: 03D15 Complexity of computation (including implicit computational complexity) 68Q25 Analysis of algorithms and problem complexity Keywords:polynomial complexity; quasipolynomial algorithms; satisfiability of propositional formulas; derivability of formulas; implicative normal forms PDFBibTeX XMLCite \textit{M. I. Kanovich}, Sov. Math., Dokl. 34, 273--277 (1987; Zbl 0629.03013); translation from Dokl. Akad. Nauk SSSR 290, 281--286 (1986)