Combination problems for commutative/monoidal theories or how algebra can help in equational unification

DOI10.1007/BF01195536zbMath0853.03008OpenAlexW2004460530MaRDI QIDQ1919702

Franz Baader, Werner Nutt

Publication date: 6 January 1997

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

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

zbMATH Keywords

algorithmsAbelian groupsequational theoriescommutative theoriesAbelian monoidsequational unificationmonoidal theoriessemiadditive categoriessystems of linear equations over a semiring

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Applications of universal algebra in computer science (08A70) Semirings (16Y60) Equational classes, universal algebra in model theory (03C05) Preadditive, additive categories (18E05)

Related Items

Restricted unification in the DL \(\mathcal{FL}_0\), Filtering unification and most general unifiers in modal logic, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Deciding Knowledge in Security Protocols for Monoidal Equational Theories, Decidability and combination results for two notions of knowledge in security protocols, Unification of concept terms in description logics, Symbolic protocol analysis for monoidal equational theories

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unification in commutative theories
• Unification in a combination of arbitrary disjoint equational theories
• The unification hierarchy is undecidable
• Complete sets of transformations for general E-unification
• Automated deduction by theory resolution
• Basic narrowing revisited
• Combination problems for commutative/monoidal theories or how algebra can help in equational unification
• Unification in commutative theories, Hilbert's basis theorem, and Gröbner bases
• A theory of complete logic programs with equality
• Completion of a Set of Rules Modulo a Set of Equations
• Extending SLD resolution to equational horn clauses using E-unification
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• 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
• Algebraic semantics for modal logics I
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES