On the complexity of equational problems in CNF

DOI10.1016/S0747-7171(03)00029-4MaRDI QIDQ1404988zbMATH OpenFDO

Authors Reinhard Pichler

Publication date 25 August 2003

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

complexityNP-completenesspolynomial hierarchyequational reasoning

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35)

Recommendations

• Automated Deduction – CADE-20
• Mathematical Foundations of Computer Science 2003
• On problems as hard as CNF-SAT
• Theory and Applications of Satisfiability Testing
• CNF satisfiability in a subspace and related problems
• On Linear CNF Formulas
• Complexity of a CHR Solver for Existentially Quantified Conjunctions of Equations over Trees
• Complexity of the problem of being equivalent to Horn formulas
• Publication:4729350
• scientific article; zbMATH DE number 3849128

Cites work

• scientific article; zbMATH DE number 176121 (Why is no real title available?)
• scientific article; zbMATH DE number 1341610 (Why is no real title available?)
• scientific article; zbMATH DE number 549974 (Why is no real title available?)
• scientific article; zbMATH DE number 592370 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• An Efficient Unification Algorithm
• Equational formulae with membership constraints
• Equational problems and disunification
• Explicit representation of terms defined by counter examples
• Hyperresolution and automated model building
• Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria

Cited in

(4)

• Generalizing DPLL and satisfiability for equalities
• Parameterized provability in equational logic
• scientific article; zbMATH DE number 1670857 (Why is no real title available?)
• The equational theory of a nontrivial discriminator variety is co-NP-hard

This page was built for publication: On the complexity of equational problems in CNF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1404988)