Lics

IEEE Symposium on Logic in Computer Science

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

Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

Paper: Unification in free extensions of Boolean rings and Abelian groups (at LICS 1988)

Authors: Alexandre Boudet Jean-Pierre Jouannaud Manfred Schmidt-Schauß

Abstract

A complete unification algorithm is presented for the combination of two arbitrary equational theories E in T(F,X) and E1 in T (F',X), where F and F' denote two disjoint sets of function symbols. The method adapts to unification of infinite trees. It is applied to two well-known open problems, when E is the theory of Boolean rings or the theory of Abelian groups, and E is the free theory. The interest to Boolean rings originates in VSLI verification

BibTeX

  @InProceedings{BoudetJouannaudSchm-Unificationinfreeex,
    author = 	 {Alexandre Boudet and Jean-Pierre Jouannaud and Manfred Schmidt-Schauß},
    title = 	 {Unification in free extensions of Boolean rings and Abelian groups },
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {121--130},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski