Unification in a combination of arbitrary disjoint equational theories (Q582270): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(5 intermediate revisions by 4 users not shown) | |||
Property / author | |||
Property / author: Manfred Schmidt-Schauss / rank | |||
Property / review text | |||
The paper extends the known results on unification in a disjoint combination of regular and collapse-free equational theories (which are unification-type finitary) in the sense that arbitrary theories are admissible. The general procedure described is based on the reduction of the problem to the pure unification problem with free constants and the constant-elimination problem in the composing theories. It provides an enumeration of a complete set of unifiers, even if some unification procedure for a particular theory produces an infinite complete set of unifiers. It is proved that unifiability of \(E_ 1+E_ 2+...+E_ n\) is decidable if for every \(i=1,...,n\) there exists a method to decide unification in a combination of the \(E_ i's\) with free function symbols. | |||
Property / review text: The paper extends the known results on unification in a disjoint combination of regular and collapse-free equational theories (which are unification-type finitary) in the sense that arbitrary theories are admissible. The general procedure described is based on the reduction of the problem to the pure unification problem with free constants and the constant-elimination problem in the composing theories. It provides an enumeration of a complete set of unifiers, even if some unification procedure for a particular theory produces an infinite complete set of unifiers. It is proved that unifiability of \(E_ 1+E_ 2+...+E_ n\) is decidable if for every \(i=1,...,n\) there exists a method to decide unification in a combination of the \(E_ i's\) with free function symbols. / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B35 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03C05 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 08B05 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 4130341 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
unification in a disjoint combination of regular and collapse-free equational theories | |||
Property / zbMATH Keywords: unification in a disjoint combination of regular and collapse-free equational theories / rank | |||
Normal rank | |||
Property / author | |||
Property / author: Manfred Schmidt-Schauss / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Cristian Masalagiu / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The theory of idempotent semigroups is of unification type zero / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5762080 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Unification in Boolean rings and Abelian groups / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3934450 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3779785 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3786017 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Matching - a special case of unification? / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5679729 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proving termination with multiset orderings / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Properties of substitutions and unifications / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3338216 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Complete sets of unifiers and matchers in equational theories / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3743300 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3782762 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Untersuchungen über das logische Schliessen. I / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4200260 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3786019 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3835440 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3674088 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3883561 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3664457 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Completion of a Set of Rules Modulo a Set of Equations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3338225 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5581665 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: New decision algorithms for finitely presented commutative semigroups / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3219154 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3338213 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4139711 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The decision problem for equational bases of algebras / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An Efficient Unification Algorithm / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3786022 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Simplification by Cooperating Decision Procedures / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Combining matching algorithms: The regular case / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Basic narrowing revisited / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear unification / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5678447 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4159023 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Machine-Oriented Logic Based on the Resolution Principle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Unification under associativity and idempotence is of type nullary / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3811748 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Computational aspects of an order-sorted logic with term declarations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3484383 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Unification Algorithm for Associative-Commutative Functions / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5609363 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3030272 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3785922 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the Church-Rosser property for the direct sum of term rewriting systems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Concept of Demodulation in Theorem Proving / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Unification in combinations of collapse-free regular theories / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 12:13, 20 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Unification in a combination of arbitrary disjoint equational theories |
scientific article |
Statements
Unification in a combination of arbitrary disjoint equational theories (English)
0 references
1989
0 references
The paper extends the known results on unification in a disjoint combination of regular and collapse-free equational theories (which are unification-type finitary) in the sense that arbitrary theories are admissible. The general procedure described is based on the reduction of the problem to the pure unification problem with free constants and the constant-elimination problem in the composing theories. It provides an enumeration of a complete set of unifiers, even if some unification procedure for a particular theory produces an infinite complete set of unifiers. It is proved that unifiability of \(E_ 1+E_ 2+...+E_ n\) is decidable if for every \(i=1,...,n\) there exists a method to decide unification in a combination of the \(E_ i's\) with free function symbols.
0 references
unification in a disjoint combination of regular and collapse-free equational theories
0 references