کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423331 685205 2006 13 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Mining Propositional Simplification Proofs for Small Validating Clauses
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Mining Propositional Simplification Proofs for Small Validating Clauses
چکیده انگلیسی

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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 144, Issue 2, 19 January 2006, Pages 79-91