Skip to Main content Skip to Navigation
Reports

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 metadata

https://hal.inria.fr/inria-00075867
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 7:29:37 PM
Last modification on : Friday, February 4, 2022 - 3:15:22 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

124

Files downloads

60