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