Justifying Equality

(Submitted for publication, 15 April 1004)

---

Authors

Leonardo de Moura and Harald Rueß and Natarajan Shankar

Abstract

We consider the problem of finding irredundant justifications for an inconsistent set of equalities and disequalities. These are subsets of input literals which do not contain any redundant literal, that is, literals which do not contribute to the unsatisfiability in an essential way, and can therefore be ignored. The approach we are pursuing here is to decorate derivations with proofs and to extract an irredundant set of assumptions from these proofs. This requires specialized operators on proofs, but the base inference systems are left unchanged. In particular, we include proof-producing inference systems for union-find structures and abstract congruence closure.

gzipped postscript or postscript or PDF

BibTeX Entry

@misc{dMRS:PDPAR04,
	TITLE = {Justifying Equality},
	AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and Natarajan Shankar},
        NOTE = {Submitted for publication, 15 April 2004},
        URL = {\url{http://www.csl.sri.com/users/ruess/papers/PDPAR04/index.html}},
}

---

Harald Ruess: ruess@csl.sri.com