Combining unification algorithms

DOI10.1006/jsco.1993.1066zbMath0822.68054OpenAlexW2083194346MaRDI QIDQ1329186

Alexandre Boudet

Publication date: 18 October 1995

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

Full work available at URL: https://doi.org/10.1006/jsco.1993.1066

zbMATH Keywords

unification algorithms

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Related Items (11)

Combination of constraint solving techniques: An algebraic point of view ⋮ AC-complete unification and its application to theorem proving ⋮ Rewriting modulo SMT and open system analysis ⋮ Combination of constraint solvers for free and quasi-free structures ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Combination of convex theories: modularity, deduction completeness, and explanation ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Unification algorithms cannot be combined in polynomial time.

This page was built for publication: Combining unification algorithms