Justifying Equality

详细信息    查看全文

• 作者：Leonardo de Moura ; Harald Rueß ; ; Natarajan Shankar
• 关键词：Decision Procedures ; Satisfiability ; Union-Find ; Congruence Closure ; Proof Theory ; Minimal Proofs
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2005
• 出版时间：18 July 2005
• 年：2005
• 卷：125
• 期：3
• 页码：69-85
• 全文大小：311 K

文摘

We consider the problem of finding irredundant bases for inconsistent sets of equalities and disequalities. These are subsets of inconsistent sets which do not contain any literals which do not contribute to the unsatisfiability in an essential way, and can therefore be discarded. The approach we are pursuing here is to decorate derivations with proofs and to extract irredundant sets of assumptions from these proofs. This requires specialized operators on proofs, but the basic inference systems are otherwise left unchanged. In particular, we include justifying inference systems for union-find structures and abstract congruence closure, but our constructions can also be applied to other inference systems such as Gaussian elimination.