“Syntactic” AC-unification

DOI10.1007/BFb0016849zbMath1495.03012OpenAlexW1555763131MaRDI QIDQ5096305

Alexandre Boudet, Evelyne Contejean

Publication date: 16 August 2022

Published in: Constraints in Computational Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bfb0016849

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Problems in rewriting III

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in abelian semigroups
• Associative-commutative unification
• Unification problems with one-sided distributivity
• AC-unification race: The system solving approach, implementation and benchmarks
• AC unification through order-sorted AC1 unification
• Competing for the \(AC\)-unification race
• Syntacticness, cycle-syntacticness and shallow theories
• An efficient incremental algorithm for solving systems of linear diophantine equations
• A Unification Algorithm for Associative-Commutative Functions
• Undecidable properties of syntactic theories