Skip to main content
SpringerLink
Log in

SAT-Enhanced Mizar Proof Checking

  • Conference paper
Intelligent Computer Mathematics (CICM 2014)

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

Included in the following conference series:

Abstract

In this paper we present an experimental extension of the Mizar system employing an external SAT solver to strengthen the notion of obviousness of the Mizar proof checker. The presented extension is based on a version of MiniSAT, called Logic2CNF. The SAT-enhanced Mizar checker is programmed to automatically spawn a new Logc2CNF process whenever it needs to justify any goal that involves equalities based on Boolean operations.

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. Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar Mathematical Library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 149–163. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  2. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135–150. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Caminati, M.B., Rosolini, G.: Custom automations in Mizar. Journal of Automated Reasoning 50(2), 147–160 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  4. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)

    MathSciNet  MATH  Google Scholar 

  5. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 235–249. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Grabowski, A., Schwarzweller, C.: Towards automatically categorizing mathematical knowledge. In: Proceedings of Federated Conference on Computer Science and Information Systems – FedCSIS 2012, Wroclaw, Poland, September 9–12, pp. 63–68 (2012)

    Google Scholar 

  7. Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. CoRR, abs/1310.2805 (2013)

    Google Scholar 

  8. Korniłowicz, A.: Tentative experiments with ellipsis in Mizar. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 453–457. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  9. Korniłowicz, A.: On rewriting rules in Mizar. Journal of Automated Reasoning 50(2), 203–210 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  10. Naumowicz, A.: An example of formalizing recent mathematical results in Mizar. Journal of Applied Logic 4(4), 396–413 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  11. Naumowicz, A.: Evaluating prospective built-in elements of computer algebra in Mizar. Studies in Logic, Grammar and Rhetoric 10(23), 191–200 (2007)

    Google Scholar 

  12. Naumowicz, A.: Interfacing external CA systems for Gröbner bases computation in Mizar proof checking. International Journal of Computer Mathematics 87(1), 1–11 (2010)

    Article  MATH  Google Scholar 

  13. Naumowicz, A., Byliński, C.: Improving Mizar texts with properties and requirements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 290–301. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 67–72. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Pąk, K.: Methods of lemma extraction in natural deduction proofs. Journal of Automated Reasoning 50(2), 217–228 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  16. Trybulec, A., Korniłowicz, A., Naumowicz, A., Kuperberg, K.: Formal mathematics for mathematicians. Journal of Automated Reasoning 50(2), 119–121 (2013)

    Article  MathSciNet  Google Scholar 

  17. Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning 50(2), 229–241 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  18. Weber, T.: Integrating a SAT solver with an LCF-style theorem prover. In: Proceedings of the Third International Workshop on Pragmatical Aspects of Decision Procedures in Automated Reasoning, PDPAR (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Białystok, Sosnowa 64, 15-887, Białystok, Poland

    Adam Naumowicz

Authors
  1. Adam Naumowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, The University of Western Ontario, MC 375,, N6A 5B7, London, ON, Canada

    Stephen M. Watt

  2. Departments of Computer Science and Mathematical Sciences, University of Bath, Claverton Down, BA2 7AY, Bath, UK

    James H. Davenport

  3. School of Computer Science, Edgbaston, University of Birmingham, B15 2TT, Birmingham, UK

    Alan P. Sexton

  4. Faculty of Informatics, Masaryk University, Botanicá 6a, 60200, Brno, Czech Republic

    Petr Sojka

  5. Institute for Computing Sciences, Radboud University Nijmegen, Postbus 9010,, 6525, Nijmegen, GL, The Netherlands

    Josef Urban

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Naumowicz, A. (2014). SAT-Enhanced Mizar Proof Checking. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_37

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08434-3_37

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08433-6

  • Online ISBN: 978-3-319-08434-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation