Abstract
This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm, RecyclePivots-WithIntersection, performs partial regularization, removing an inference η when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference located below in the path from η to the root of the proof. The second algorithm, LowerUnits, delays the resolution of (both input and derived) unit clauses, thus removing (some) inferences having the same pivot but possibly occurring also in different branches of the proof.
This work was partly supported by the ANR DeCert project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. Hardware and Software: Verification and Testing, 114–128 (2009)
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)
Bouton, T., de Oliveira, D. C.B., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009)
Cotton, S.: Two techniques for minimizing resolution proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306–312. Springer, Heidelberg (2010)
Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploring and Exploiting Algebraic and Graphical Properties of Resolution. In: 8th International Workshop on Satisfiability Modulo Theories (Part of FLoC - Federated Logic Conferences) (2010)
Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 106–119. ACM, New York (1997)
Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima Press (2008)
Simone, S., Brutomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: 6th Haifa Verification Conference (2010)
Tseitin, G.: On the complexity of proofs in propositional logics. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic, vol. 2, pp. 1967–1970. Springer, Heidelberg (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fontaine, P., Merz, S., Woltzenlogel Paleo, B. (2011). Compression of Propositional Resolution Proofs via Partial Regularization. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-22438-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22437-9
Online ISBN: 978-3-642-22438-6
eBook Packages: Computer ScienceComputer Science (R0)