Solving disequations

Abstract : We present a general study of equations (objects of form s=t and disequations (objects of form s \ne 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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00075867
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 7:29:37 PM
Last modification on : Saturday, September 17, 2016 - 1:06:54 AM
Long-term archiving on : Friday, May 13, 2011 - 3:57:07 PM

Identifiers

  • HAL Id : inria-00075867, version 1

Collections

Citation

Claude Kirchner, Pierre Lescanne. Solving disequations. [Research Report] RR-0686, INRIA. 1987. ⟨inria-00075867⟩

Share

Metrics

Record views

158

Files downloads

103