Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: Syntactic theories and unification (at LICS 1990)

Authors: Kirchner, C. Klay, F.


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


    author = 	 {Kirchner, C. and Klay, F.},
    title = 	 {Syntactic theories and unification},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {270--277},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}