Combining matching algorithms: The regular case

DOI10.1007/3-540-51081-8_118zbMath1503.68315OpenAlexW2052053628MaRDI QIDQ5055731

Tobias Nipkow

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-51081-8_118

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42) Word problems, etc. in computability and recursion theory (03D40) Equational classes, universal algebra in model theory (03C05)

Related Items

Second-order unification in the presence of linear shallow algebraic equations, Modular higher-order E-unification, Combination techniques for non-disjoint equational theories, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method

Uses Software

• LARCH

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in combinations of collapse-free regular theories
• 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
• Complete Sets of Reductions for Some Equational Theories
• An overview of LP, the Larch Prover