Unification in a combination of arbitrary disjoint equational theories (Q582270): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
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 / reviewed by | |||
Property / reviewed by: Q593640 / 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 |
Revision as of 19:05, 1 July 2023
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