## Paper: Syntactic theories and unification (at LICS 1990)

**Claude Kirchner Francis Klay**

### Abstract

An investigation is made of the relationship between unifiability of a general equation of the form f(ν_{1}, . . ., ν_{n})=^{?}g(ν_{n+1}, . . ., ν _{m}), and of the syntacticness of the theory. After introducing the concept of general equations and its basic properties, the
precise definition of syntactic theories is given. It is proven that a theory is syntactic if and only is the general equations
have finite complete set of E-solutions. The result is constructive in the sense that from the E-solutions of the general
equations, a resolvent presentation is computed. This is applied to several theories: in particular, in order to show that
distributivity is not syntactic. The authors also prove that the theory of associativity and commutativity is syntactic, which
allows one, by the combination of Nipkow's results (ibid., p.278-88, 1990) and the authors', to infer a novel matching algorithm
where there is no need to solve linear diophantine equations

### BibTeX

@InProceedings{KirchnerKlay-Syntactictheoriesan, author = {Claude Kirchner and Francis Klay}, title = {Syntactic theories and unification}, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {270--277}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }