Paper: Solving Disequations (at LICS 1987)

Authors: Claude Kirchner Pierre Lescanne

Abstract

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.

BibTeX

  @InProceedings{KirchnerLescanne-SolvingDisequations,
    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}
  }