Unification in Boolean rings and Abelian groups

DOI10.1016/S0747-7171(89)80054-9zbMath0689.68040WikidataQ55878423 ScholiaQ55878423MaRDI QIDQ582073

Jean-Pierre Jouannaud, Alexandre Boudet, Manfred Schmidt-Schauss

Publication date: 1989

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

zbMATH Keywords

arbitrary equational theoriescomplete unification algorithmVLSI verification

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65) Ring-theoretic properties of Boolean algebras (06E20)

Related Items

On the complexity of Boolean unification ⋮ Unification in commutative semigroups ⋮ Abstract data type systems ⋮ Efficient general AGH-unification ⋮ Towards Parallel Boolean Functional Synthesis ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Boolean functional synthesis: hardness and practical algorithms ⋮ Tactics for Reasoning Modulo AC in Coq ⋮ On equational theories, unification, and (un)decidability ⋮ Unification algorithms cannot be combined in polynomial time.

Cites Work

• Associative-commutative unification
• Automata, languages and programming. 10th Colloquium, Barcelona, Spain, Juli 18-22, 1983
• Deciding Combinations of Theories
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• Characterizations of unification type zero
• On the Church-Rosser property for the direct sum of term rewriting systems
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Unification in Boolean rings and Abelian groups