Associative-commutative unification

DOI10.1016/S0747-7171(87)80004-4zbMath0638.68103WikidataQ56092434 ScholiaQ56092434MaRDI QIDQ1099648

François Fages

Publication date: 1987

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

zbMATH Keywords

correctnessterminationautomated deductionequational theoriesUnificationassociative- commutative functionshomogeneous linear diophantine equations

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05) Linear Diophantine equations (11D04)

Related Items

Open problems in rewriting, AC-complete unification and its application to theorem proving, Unnamed Item, Efficient solution of linear diophantine equations, Permutative rewriting and unification, “Syntactic” AC-unification, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Nominal AC-matching, A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols, On the unification problem for Cartesian closed categories, Unification algorithms cannot be combined in polynomial time, A new method for undecidability proofs of first order theories, Building Theorem Provers, Unification in Boolean rings and Abelian groups, On pot, pans and pudding or how to discover generalised critical Pairs, Adventures in associative-commutative unification, Unification in permutative equational theories is undecidable, A formalisation of nominal C-matching through unification with protected variables, Unification algorithms cannot be combined in polynomial time., Formalising nominal C-unification generalised with protected variables, Competing for the \(AC\)-unification race

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
• Complete sets of unifiers and matchers in equational theories
• On the sequential nature of unification
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• Complete Sets of Reductions for Some Equational Theories
• Hilbert's Tenth Problem is Unsolvable
• A Machine-Oriented Logic Based on the Resolution Principle