Unification algorithms cannot be combined in polynomial time.
From MaRDI portal
Mechanization of proofs and logical operations (03B35) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)
Recommendations
- Unification algorithms cannot be combined in polynomial time
- Tractable and intractable instances of combination problems for unification and disunification
- A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms
- Combining unification algorithms
- Unification in a combination of equational theories: an efficient algorithm
Cites work
- A Unification Algorithm for Associative-Commutative Functions
- Associative-commutative unification
- Boolean unification - the story so far
- Combination of constraint solving techniques: An algebraic point of view
- Combination techniques for non-disjoint equational theories
- Combining decision algorithms for matching in the union of disjoint equational theories
- Combining matching algorithms: The regular case
- Combining symbolic constraint solvers on algebraic domains
- Combining unification algorithms
- Complete sets of unifiers and matchers in equational theories
- Complexity of unification problems with associative-commutative operators
- Computational complexity of simultaneous elementary matching problems
- scientific article; zbMATH DE number 3888913 (Why is no real title available?)
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4049130 (Why is no real title available?)
- scientific article; zbMATH DE number 592370 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1142309 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- Polynomial Algorithms for Computing the Smith and Hermite Normal Forms of an Integer Matrix
- The complexity of computing the permanent
- The complexity of counting problems in equational matching
- The Complexity of Enumeration and Reliability Problems
- The complexity of theorem-proving procedures
- Unification and matching modulo nilpotence
- Unification in a combination of arbitrary disjoint equational theories
- Unification in abelian semigroups
- Unification in Boolean rings
- Unification in Boolean rings and Abelian groups
- Unification in combinations of collapse-free regular theories
- Unification in the union of disjoint equational theories: Combining decision procedures
Cited in
(6)- scientific article; zbMATH DE number 4037063 (Why is no real title available?)
- scientific article; zbMATH DE number 2064226 (Why is no real title available?)
- A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms
- Unification algorithms cannot be combined in polynomial time
- Tractable and intractable instances of combination problems for unification and disunification
- Unification in Boolean rings and Abelian groups
This page was built for publication: Unification algorithms cannot be combined in polynomial time.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1854364)
