Equational problems and disunification - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 1988

Equational problems and disunification

Hubert Comon
  • Function : Author
Pierre Lescanne
  • Function : Author


Roughly speaking, an equational problem is a first order formula whose only predicate symbol is =. We propose some rules for the transformation of equational problems and study their correctness in various models. Then, we give completeness results with respect to some "simple" problems called solved forms. Such completeness results still hold when adding some control which moreover ensures termination. The termination proofs are given for a "weak" control and thus hold for the (large) class of algorithms obtained by restricting the scope of the rules. Finally, it must be noted that a by-product of our method is a decision procedure for the validity in the Herbrand Universe of any first order formula with the only predicate symbol =.
Fichier principal
Vignette du fichier
RR-0904.pdf (2.12 Mo) Télécharger le fichier

Dates and versions

inria-00075652 , version 1 (24-05-2006)


  • HAL Id : inria-00075652 , version 1


Hubert Comon, Pierre Lescanne. Equational problems and disunification. [Research Report] RR-0904, INRIA. 1988. ⟨inria-00075652⟩
94 View
83 Download


Gmail Facebook Twitter LinkedIn More