Combining matching algorithms: The regular case

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

Tobias Nipkow

Publication date: 28 June 1992

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

zbMATH Keywords

combination problem; combining matching algorithms; equational theories with disjoint signatures

Mathematics Subject Classification ID

68W30: Symbolic computation and algebraic computation

03C05: Equational classes, universal algebra in model theory

Related Items

Unification in a combination of arbitrary disjoint equational theories, Combining word problems through rewriting in categories with products, Maude: specification and programming in rewriting logic, Unions of non-disjoint theories and combinations of satisfiability procedures, Unification algorithms cannot be combined in polynomial time., A new combination procedure for the word problem that generalizes fusion decidability results in modal logics

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