ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: Syntactic theories and unification (at LICS 1990)

Authors: Claude Kirchner Francis Klay


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 = 	 {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}

Last modified: 2022-10-3113:49
Sam Staton