zbMATH — the first resource for mathematics

A unified proof system for QBF preprocessing. (English) Zbl 1409.68257
Demri, StĂ©phane (ed.) et al., Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19–22, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8562, 91-106 (2014).
Summary: For quantified Boolean formulas (QBFs), preprocessing is essential to solve many real-world formulas. The application of a preprocessor, however, prevented the extraction of proofs for the original formula. Such proofs are required to independently validate correctness of the preprocessor’s rewritings and the solver’s result. Especially for universal expansion proof checking was not possible so far. In this paper, we introduce a unified proof system based on three simple and elegant quantified resolution asymmetric tautology (QRAT) rules. In combination with an extended version of universal reduction, they are sufficient to efficiently express all preprocessing techniques used in state-of-the-art preprocessors including universal expansion. Moreover, these rules give rise to new preprocessing techniques. We equip our preprocessor bloqqer with QRAT proof logging and provide a proof checker for QRAT proofs.
For the entire collection see [Zbl 1293.68021].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: DOI