ACM/IEEE Symposium on Logic in Computer Science

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

Second Annual IEEE Symposium on

Logic in Computer Science (LICS 1987)

Paper: Solving Disequations (at LICS 1987)

Authors: Claude Kirchner Pierre Lescanne


We present a general study of equations (objects of form s=t) and disequations (objects of form s≠t) solving. The problem is approached from its fully general mathematical definition clearly separating universally and existentially quantified variables. In addition it is showed to have many connections with unification in equational theories like associativity commutativity, in particular methods similar to those used to solve equational unification problem works in solving disequations. This abstract framework is then applied to study the sufficient completeness of a rewrite rule based definition of a function.


    author = 	 {Claude Kirchner and Pierre Lescanne},
    title = 	 {Solving Disequations},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {347--352},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}

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