Permutative rewriting and unification

DOI10.1016/J.IC.2006.11.001MaRDI QIDQ876048zbMATH OpenOpenAlexFDO

Authors Thierry Boy de la Tour, Mnacho Echenim

Publication date 16 April 2007

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2006.11.001

zbMATH Keywords

term rewritingequational theoriespermutation groups\(E\)-unification

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Term Rewriting and Applications
• Unification and Matching Modulo Leaf-Permutative Equational Presentations
• Unification in permutative equational theories is undecidable
• Some results on equational unification
• Single versus simultaneous equational unification and equational unification for variable-permuting theories

Cites work

• scientific article; zbMATH DE number 48157 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 2090320 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• An algebraic approach to unification under associativity and commutativity
• Associative-commutative unification
• Automated Reasoning
• Decidability and complexity analysis by basic paramodulation
• Fundamental algorithms for permutation groups
• Group-theoretic algorithms and graph isomorphism
• Single versus simultaneous equational unification and equational unification for variable-permuting theories
• Term Rewriting and Applications
• Unification in commutative theories, Hilbert's basis theorem, and Gröbner bases
• Unification in permutative equational theories is undecidable
• Unification theory

Cited in

(7)

• Uniform rewriting based on permutations
• Automated Reasoning
• On First-Order Model-Based Reasoning
• Term Rewriting and Applications
• Unification and Matching Modulo Leaf-Permutative Equational Presentations
• General algorithms for permutations in equational inference
• Restricted combinatory unification

This page was built for publication: Permutative rewriting and unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q876048)