zbMATH — the first resource for mathematics

The taming of the (X)OR. (English) Zbl 0983.68174
Lloyd, John (ed.) et al., Computational logic - CL 2000. 1st international conference, London, GB, July 24-28, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1861, 508-522 (2000).
Summary: Many key verification problems such as bounded model-checking, circuit verification and logical cryptanalysis are formalized with combined clausal and affine logic (i.e. clauses with xor as the connective) and cannot be efficiently (if at all) solved by using CNF-only provers.
We present a decision procedure to efficiently decide such problems. The Gauss-DPLL procedure is a tight integration in a unifying framework of a Gauss-Elimination procedure (for affine logic) and a Davis-Putnam-Logeman-Loveland procedure (for usual clause logic).
The key idea, which distinguishes our approach from others, is the full interaction bewteen the two parts which makes it possible to maximize (deterministic) simplification rules by passing around newly created unit or binary clauses in either of these parts. We show the correcteness and the termination of Gauss-DPLL under very liberal assumptions.
For the entire collection see [Zbl 0941.00011].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX Cite