Deciding Propositional Combinations of Equalities and Inequalities

Submitted for publication

---

Authors

Jean-Christophe Filliatre, Sam Owre, Harald Rueß, and N. Shankar

Abstract

We describe a procedure for deciding a rich theory with both interpreted and uninterpreted function symbols. The language of this theory includes equalities, disequalities, arithmetic operators and inequalities, and propositions. Our combination algorithm is a natural extension of the equality and disequality decision procedure by Rueß and Shankar. We use canonization with respect to a congruence-closed partition as a shared operation among the individual theories. Another characteristic of our decision procedure is its laziness in processing nonatomic propositions.

gzipped postscript or postscript

BibTeX Entry

@unpublished{FilliatreOwreRuessShankar:2001,
  TITLE = {Deciding Propositional Combinations of Equalities and Inequalities},
  AUTHOR = {Jean-Christophe Filli{\^a}tre and Sam Owre and Harald Rue{\ss} and N. Shankar},
  YEAR = 2001,
  NOTE = {Submitted for publication}
}

---

Harald Ruess: ruess@csl.sri.com