Unification theory
From MaRDI portal
Publication:6169561
DOI10.1007/3-540-55124-7_5zbMath1518.68151OpenAlexW4254096036MaRDI QIDQ6169561
Publication date: 14 August 2023
Published in: Word Equations and Related Topics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-55124-7_5
Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Restricted unification in the DL \(\mathcal{FL}_0\) ⋮ On unification and admissible rules in Gabbay-de Jongh logics ⋮ DECIDABILITY OF ADMISSIBILITY: ON A PROBLEM BY FRIEDMAN AND ITS SOLUTION BY RYBAKOV
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unification under associativity and idempotence is of type nullary
- The theory of idempotent semigroups is of unification type zero
- Unification in commutative theories
- Unification in a combination of arbitrary disjoint equational theories
- Hilbert's tenth problem is of unification type zero
- Complexity of unification problems with associative-commutative operators
- Unification in varieties of idempotent semigroups
- Unification in abelian semigroups
- Unification in combinations of collapse-free regular theories
- Unification in commutative idempotent monoids
- Efficient solution of linear diophantine equations
- Unification theory
- Linear unification
- Automated deduction by theory resolution
- Basic narrowing revisited
- On equational theories, unification, and (un)decidability
- The undecidability of the DA-unification problem
- A theory of complete logic programs with equality
- Completion of a Set of Rules Modulo a Set of Equations
- Unification: a multidisciplinary survey
- 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
- Efficiency of a Good But Not Linear Set Union Algorithm
- A Human Oriented Logic for Automatic Theorem-Proving
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: Unification theory
