On the complexity of equational problems in CNF

DOI10.1016/S0747-7171(03)00029-4zbMath1019.03010MaRDI QIDQ1404988

Reinhard Pichler

Publication date: 25 August 2003

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

zbMATH Keywords

complexityNP-completenessequational reasoningpolynomial hierarchy

Mathematics Subject Classification ID

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

Related Items (1)

Generalizing DPLL and satisfiability for equalities

Cites Work

• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Equational formulae with membership constraints
• An Efficient Unification Algorithm
• Hyperresolution and automated model building
• A Machine-Oriented Logic Based on the Resolution Principle
• Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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