Combining matching algorithms: The regular case

DOI10.1016/S0747-7171(08)80145-9zbMath0767.68069OpenAlexW2075212034MaRDI QIDQ1186723

Tobias Nipkow

Publication date: 28 June 1992

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(08)80145-9

zbMATH Keywords

combination problemcombining matching algorithmsequational theories with disjoint signatures

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Equational classes, universal algebra in model theory (03C05)

Related Items

Combining word problems through rewriting in categories with products, Unification and Matching in Hierarchical Combinations of Syntactic Theories, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Anti-patterns for rule-based languages, Unification in a combination of arbitrary disjoint equational theories, Termination Modulo Combinations of Equational Theories, 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., Maude: specification and programming in rewriting logic

Uses Software

• LARCH
• REVE

Cites Work

• Unification in a combination of arbitrary disjoint equational theories
• Matching - a special case of unification?
• Unification in combinations of collapse-free regular theories
• Unification theory
• Completion of a Set of Rules Modulo a Set of Equations
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• An Efficient Unification Algorithm
• Complete Sets of Reductions for Some Equational Theories
• An overview of LP, the Larch Prover
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item