On n-syntactic equational theories
Alexandre Boudet and Evelyne Contejean
Abstract: We define the n-syntactic theories as a natural extension of the syntactic theories. A n-syntactic theory is an equational theory which admits a finite presentation in which every proof can be performed with at most n applications of an axiom at the root,but no finite presentation in which every proof can be performed with at most n−1 applications of an axiom at the root. The n-syntactic theories inherit the good properties of the syntactic theories for solving the word problem, or matching or unification problems. We show that for any integer n≥ 1, there exists a n-syntactic theory.
This document was translated from LATEX by HEVEA.