Unification properties of commutative theories: A categorical treatment

DOI10.1007/BFb0018357zbMath1496.03036OpenAlexW1530951877MaRDI QIDQ5096265

Franz Baader

Publication date: 16 August 2022

Published in: Category Theory and Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Unification, weak unification, upper bound, lower bound, and generalization problems ⋮ Adding homomorphisms to commutative/monoidal theories or how algebra can help in equational unification

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
• A theory of complete logic programs with equality
• 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
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Characterizations of unification type zero
• 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
• Unnamed Item