Skip to main content
SpringerLink
Log in

Skeptik: A Proof Compression System

  • Conference paper
Automated Reasoning (IJCAR 2014)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8562))

Included in the following conference series:

Abstract

This paper introduces Skeptik: a system for checking, compressing and improving proofs obtained by SAT- and SMT-solvers.

Funded by Google Summer of Code 2012 and 2013 and FWF project P24300.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Reducing the size of resolution proofs in linear time. STTT 13(3), 263–272 (2011)

    Article  Google Scholar 

  3. Biere, A.: Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, JSAT (2008)

    Google Scholar 

  4. Boudou, J., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs by lowering subproofs. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 59–73. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. 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 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Woltzenlogel Paleo, B.: Prooftool: a gui for the gapt framework. In: UITP, pp. 1–14 (2013)

    Google Scholar 

  8. Dunchev, T., Leitsch, A., Libal, T., Weller, D., Woltzenlogel Paleo, B.: System description: The proof transformation system ceres. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 427–433. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 237–251. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. Gilbert, J.R., Lengauer, T., Tarjan, R.E.: The pebbling problem is complete in polynomial space. SIAM Journal on Computing 9(3), 513–524 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  11. Goerdt, A.: Comparing the complexity of regular and unrestricted resolution. In: Marburger, H. (ed.) GWAI. Informatik-Fachberichte, vol. 251. Springer (1990)

    Google Scholar 

  12. Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC/Calculemus/MKM 2008. LNCS (LNAI), vol. 5144, pp. 462–477. Springer, Heidelberg (2008)

    Google Scholar 

  13. Heule, M., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD, pp. 181–188 (2013)

    Google Scholar 

  14. Hofferek, G., Gupta, A., Könighofer, B., Jiang, J.H.R., Bloem, R.: Synthesizing multiple boolean functions using interpolation on a single proof. In: FMCAD, pp. 77–84 (2013)

    Google Scholar 

  15. Rollini, S.F., Bruttomesso, R., Sharygina, N.: An efficient and flexible approach to resolution proof reduction. In: Raz, O. (ed.) HVC 2010. LNCS, vol. 6504, pp. 182–196. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967-1970, vol. 2. Springer (1983)

    Google Scholar 

  17. Woltzenlogel Paleo, B.: Atomic cut introduction by resolution: Proof structuring and compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 463–480. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Woltzenlogel Paleo, B.: Contextual natural deduction. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 372–386. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT, Université de Toulouse, France

    Joseph Boudou

  2. Free University of Bolzano, Italy

    Andreas Fellner

  3. Vienna University of Technology, Austria

    Andreas Fellner & Bruno Woltzenlogel Paleo

Authors
  1. Joseph Boudou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Fellner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bruno Woltzenlogel Paleo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS,, New York University &amp, USA

    Stéphane Demri

  2. Department of Computer Science, University of New Mexico, 87131-0001, Albuquerque, NM, USA

    Deepak Kapur

  3. Max Planck Institute for Informatics, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Boudou, J., Fellner, A., Woltzenlogel Paleo, B. (2014). Skeptik: A Proof Compression System. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08587-6_29

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08586-9

  • Online ISBN: 978-3-319-08587-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation