The undecidability of the unification and matching problem for canonical theories (Q1077931): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1007/bf00264362 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2008100839 / rank | |||
Normal rank | |||
Latest revision as of 10:46, 30 July 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | The undecidability of the unification and matching problem for canonical theories |
scientific article |
Statements
The undecidability of the unification and matching problem for canonical theories (English)
0 references
1987
0 references
The problem whether there exists a unifying substitution for two terms is considered in the class of theories which can be embedded into canonical term rewriting systems. The problem is shown to be undecidable, even if we restrict the substitutions to matching ones. This implies that the class of admissible canonical theories is a proper subset of the class of canonical theories.
0 references
term rewriting systems
0 references
admissible canonical theories
0 references
