Unification in commutative theories

DOI10.1016/S0747-7171(89)80055-0zbMath0689.68039WikidataQ57383756 ScholiaQ57383756MaRDI QIDQ582071

Franz Baader

Publication date: 1989

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

zbMATH Keywords

unificationcommutative theories

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Related Items (13)

Restricted unification in the DL \(\mathcal{FL}_0\) ⋮ Unification, weak unification, upper bound, lower bound, and generalization problems ⋮ Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification ⋮ Filtering unification and most general unifiers in modal logic ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Unification in varieties of completely regular semigroups ⋮ Decidability and combination results for two notions of knowledge in security protocols ⋮ Efficient general AGH-unification ⋮ Unification theory ⋮ Unification of concept terms in description logics ⋮ Unification modulo ACUI plus distributivity axioms ⋮ Unification in the Description Logic $\mathcal{EL}$ ⋮ Unification problem in equational theories

Cites Work

• Unification in varieties of idempotent semigroups
• Unification in commutative idempotent monoids
• An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
• Complete sets of unifiers and matchers in equational theories
• Automated deduction by theory resolution
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Human Oriented Logic for Automatic Theorem-Proving
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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 commutative theories