Justifying Equality

---

In: Proceedings of PDPAR'04, Electronic Notes in Theoretical Computer Science 68 No. 5 (2004).

Authors

Leonardo de Moura, 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.

Download: PS, 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}},
} 

---

Leonardo de Moura: demoura@csl.sri.com