Unification problem in equational theories

DOI10.1007/BF02733227zbMATH Open0919.68116MaRDI QIDQ1280985FDOQ1280985

Authors S. L. Kryvyi

Publication date 15 March 1999

Published in Cybernetics and Systems Analysis (Search for Journal in Brave)

zbMATH Keywords

universal algebras

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Model-theoretic aspects of unification
• Algebraic and logical aspects of unification
• Unification through projectivity
• scientific article; zbMATH DE number 3871321
• scientific article; zbMATH DE number 1552528

Cites work

• scientific article; zbMATH DE number 3885353 (Why is no real title available?)
• scientific article; zbMATH DE number 3871321 (Why is no real title available?)
• scientific article; zbMATH DE number 3871322 (Why is no real title available?)
• scientific article; zbMATH DE number 3871334 (Why is no real title available?)
• scientific article; zbMATH DE number 3827203 (Why is no real title available?)
• scientific article; zbMATH DE number 3900185 (Why is no real title available?)
• scientific article; zbMATH DE number 3930337 (Why is no real title available?)
• scientific article; zbMATH DE number 4049128 (Why is no real title available?)
• scientific article; zbMATH DE number 4049130 (Why is no real title available?)
• scientific article; zbMATH DE number 3577484 (Why is no real title available?)
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 1346492 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3407957 (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
• A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
• A unification algorithm for typed \(\overline\lambda\)-calculus
• An Efficient Unification Algorithm
• Boolean unification - the story so far
• Complexity of matching problems
• Complexity of the unification algorithm for first-order expressions
• DIOPHANTINE SETS
• Efficient solution of linear diophantine equations
• Embedding Boolean expressions into logic programming
• Hilbert's tenth problem is of unification type zero
• Linear unification
• Minimal and complete word unification
• The theory of idempotent semigroups is of unification type zero
• The undecidability of the D_A-unification problem
• Unification in a combination of arbitrary disjoint equational theories
• Unification in abelian semigroups
• Unification in commutative idempotent monoids
• Unification in commutative theories
• Unification problems with one-sided distributivity
• Unification under associativity and idempotence is of type nullary

Cited in

(8)

• Unification theories: examples and applications
• The undecidability of the unification and matching problem for canonical theories
• A note on a canonical theory with undecidable unification and matching problem
• scientific article; zbMATH DE number 1222419 (Why is no real title available?)
• Variant-based equational anti-unification
• Model-theoretic aspects of unification
• Deciding the word problem in the union of equational theories.
• Narrowing based procedures for equational disunification

This page was built for publication: Unification problem in equational theories

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