A generalization of the notions of matching and unrestricted unification - so-called variable-restricted unification - is proposed. The author investigates relationships between matching and unification and shows that for collapse-free theories (i.e. for theories where a non-variable term is never E-equal to a variable) matching and unification have similar behavior with respect to the existence and the cardinality of minimal complete sets of solutions. Some counter-examples where matching and unification behave differently are presented. It is shown that the existence of solutions is decidable for the unification problem but is undecidable for the matching problem. Since the matching problem may be reduced to a unification problem by introducing new free constants in signature, these counterexamples show that a decidable unification problem may become undecidable after adding free constants to a signature.
- Some results on equational unification
- The undecidability of the unification and matching problem for canonical theories
- Single versus simultaneous equational unification and equational unification for variable-permuting theories
- Combining decision algorithms for matching in the union of disjoint equational theories
- Complete sets of unifiers and matchers in equational theories
- Complete sets of unifiers and matchers in equational theories
- Equational problems and disunification
- scientific article; zbMATH DE number 4018416 (Why is no real title available?)
- scientific article; zbMATH DE number 3843132 (Why is no real title available?)
- scientific article; zbMATH DE number 3867289 (Why is no real title available?)
- scientific article; zbMATH DE number 3871321 (Why is no real title available?)
- scientific article; zbMATH DE number 4155934 (Why is no real title available?)
- scientific article; zbMATH DE number 3945372 (Why is no real title available?)
- scientific article; zbMATH DE number 4041328 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 4049126 (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 4049131 (Why is no real title available?)
- scientific article; zbMATH DE number 4080961 (Why is no real title available?)
- scientific article; zbMATH DE number 3751028 (Why is no real title available?)
- scientific article; zbMATH DE number 3639689 (Why is no real title available?)
- scientific article; zbMATH DE number 3019695 (Why is no real title available?)
- Equational unification, word unification, and 2nd-order equational unification
- Combining matching algorithms: The regular case
- Reduction rules for resolution-based systems
- Competing for the \(AC\)-unification race
- Complete sets of unifiers and matchers in equational theories
- Complexity of nilpotent unification and matching problems.
- A remark on infinite matching vs infinite unification
- Tractable and intractable second-order matching problems
- scientific article; zbMATH DE number 1722712 (Why is no real title available?)
- scientific article; zbMATH DE number 4085639 (Why is no real title available?)
- Modular higher-order E-unification
- Some independence results for equational unification
- Unification in a combination of arbitrary disjoint equational theories
- Unification of concept terms in description logics
- Unification in a combination of equational theories: an efficient algorithm
This page was built for publication: Matching - a special case of unification?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q582272)
