Journal article
Mining Propositional Simplification Proofs for Small Validating Clauses
Electronic notes in theoretical computer science, Vol.144(2), pp.79-91
01/19/2006
DOI: 10.1016/j.entcs.2005.12.008
Abstract
The problem of obtaining small conflict clauses in SMT systems has received a great deal of attention recently. We report work in progress to find small subsets of the current partial assignment that imply the goal formula when it has been propositionally simplified to a boolean value. The approach used is algebraic proof mining. Proofs from a propositional reasoner that the goal is equivalent to a boolean value (in the current assignment) are viewed as first-order terms. An equational theory between proofs is then defined, which is sound with respect to the quasi-order “proves a more general set theorems.” The theory is completed to obtain a convergent rewrite system that puts proofs into a canonical form. While our canonical form does not use the smallest subset of the current assignment, it does drop many unnecessary parts of the proof. The paper concludes with discussion of the complexity of the problem and effectiveness of the approach.
Details
- Title: Subtitle
- Mining Propositional Simplification Proofs for Small Validating Clauses
- Creators
- Ian Wehrman - Washington University in St. LouisAaron Stump - Washington University in St. Louis
- Resource Type
- Journal article
- Publication Details
- Electronic notes in theoretical computer science, Vol.144(2), pp.79-91
- DOI
- 10.1016/j.entcs.2005.12.008
- ISSN
- 1571-0661
- eISSN
- 1571-0661
- Publisher
- Elsevier B.V
- Language
- English
- Date published
- 01/19/2006
- Academic Unit
- Computer Science
- Record Identifier
- 9984259408102771
Metrics
3 Record Views