Unification in Boolean rings and Abelian groups

DOI10.1016/S0747-7171(89)80054-9MaRDI QIDQ582073zbMATH OpenWikidataFDO

Authors Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß

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)

Recommendations

• Unification in Boolean rings
• scientific article; zbMATH DE number 4080961
• scientific article; zbMATH DE number 4049133
• On the complexity of Boolean unification
• Unification algorithms cannot be combined in polynomial time.

Cites work

• scientific article; zbMATH DE number 4016226 (Why is no real title available?)
• scientific article; zbMATH DE number 3885353 (Why is no real title available?)
• scientific article; zbMATH DE number 3829296 (Why is no real title available?)
• scientific article; zbMATH DE number 3945372 (Why is no real title available?)
• scientific article; zbMATH DE number 4045129 (Why is no real title available?)
• scientific article; zbMATH DE number 4049025 (Why is no real title available?)
• scientific article; zbMATH DE number 4049133 (Why is no real title available?)
• scientific article; zbMATH DE number 4080961 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• Associative-commutative unification
• Automata, languages and programming. 10th Colloquium, Barcelona, Spain, Juli 18-22, 1983
• Characterizations of unification type zero
• Deciding Combinations of Theories
• On the Church-Rosser property for the direct sum of term rewriting systems

Cited in

(14)

• Unification algorithms cannot be combined in polynomial time.
• Boolean functional synthesis: hardness and practical algorithms
• Towards Parallel Boolean Functional Synthesis
• On equational theories, unification, and (un)decidability
• Unification in commutative semigroups
• Unification algorithms cannot be combined in polynomial time
• scientific article; zbMATH DE number 4049133 (Why is no real title available?)
• On the complexity of Boolean unification
• Abstract data type systems
• Unification in a combination of arbitrary disjoint equational theories
• Efficient general AGH-unification
• Unification in Boolean rings
• Tactics for Reasoning Modulo AC in Coq
• Unification in a combination of equational theories: an efficient algorithm

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

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