Document Open Access Logo

A Natural Formalization of the Mutilated Checkerboard Problem in Naproche

Authors Adrian De Lon, Peter Koepke, Anton Lorenzen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.16.pdf
  • Filesize: 0.6 MB
  • 11 pages

Document Identifiers

Author Details

Adrian De Lon
  • Universität Bonn, Germany
Peter Koepke
  • Universität Bonn, Germany
Anton Lorenzen
  • Universität Bonn, Germany

Cite AsGet BibTex

Adrian De Lon, Peter Koepke, and Anton Lorenzen. A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.16

Abstract

Naproche is an emerging natural proof assistant that accepts input in a controlled natural language for mathematics, which we have integrated with LaTeX for ease of learning and to quickly produce high-quality typeset documents. We present a self-contained formalization of the Mutilated Checkerboard Problem in Naproche, following a proof sketch by John McCarthy. The formalization is embedded in detailed literate style comments. We also briefly describe the Naproche approach.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • checkerboard
  • formalization
  • formal mathematics
  • controlled language

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101-148, January 2016. URL: https://doi.org/10.6092/issn.1972-5787/4593.
  2. Naproche contributors. FLib. URL: https://github.com/naproche-community/FLib.
  3. Marcos Cramer. Proof-checking mathematical texts in controlled natural language. PhD thesis, University of Bonn, 2013. Google Scholar
  4. Steffen Frerix and Peter Koepke. Automatic proof-checking of ordinary mathematical texts. Proceedings of the Workshop Formal Mathematics for Mathematicians, 2018. Google Scholar
  5. Isabelle contributors. The Isabelle2021 release, February 2021. URL: https://isabelle.in.tum.de.
  6. John L. Kelley. General Topology. Springer-Verlag New York, 1975. Google Scholar
  7. Manfred Kerber and Martin Pollet. A tough nut for mathematical knowledge management. In Michael Kohlhase, editor, Mathematical Knowledge Management, pages 81-95, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11618027_6.
  8. Donald E. Knuth. Literate Programming. Center for the Study of Language and Information, 1992. Google Scholar
  9. Peter Koepke. Textbook mathematics in the Naproche-SAD system. Joint Proceedings of the FMM and LML Workshops, 2019. Google Scholar
  10. Peter Koepke, Anton Lorenzen, and Adrian De Lon. Interpreting mathematical texts in Naproche-SAD. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, pages 284-289. Springer, 2020. Google Scholar
  11. Daniel Kühlwein, Marcos Cramer, Peter Koepke, and Bernhard Schröder. The Naproche system, January 2009. Google Scholar
  12. John McCarthy. Tough nut for proof procedures, 1964. Stanford AI Memo. Google Scholar
  13. John McCarthy. The mutilated checkerboard in set theory, 2001. Google Scholar
  14. Anthony Perry Morse; Trevor J McMinn. A theory of sets. New York ; London : Academic press, 1965. Google Scholar
  15. Andrei Paskevich. Méthodes de formalisation des connaissances et des raisonnements mathématiques: aspects appliqués et théoriques. PhD thesis, Université Paris 12, 2007. Google Scholar
  16. Andrei Paskevich. The syntax and semantics of the ForTheL language, 2007. Google Scholar
  17. Lawrence C. Paulson. ALEXANDRIA: Large-scale formal proof for the working mathematician. URL: https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/.
  18. Stephan Schulz. The E theorem prover. URL: https://eprover.org.
  19. Konstantin Verchinine, Alexander Lyaletski, and Andrei Paskevich. System for automated deduction (SAD): a tool for proof verification. Automated Deduction-CADE-21, pages 398-403, 2007. URL: https://doi.org/10.1007/978-3-540-73595-3_29.
  20. Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich, and Anatoly Anisimov. On correctness of mathematical texts from a logical and practical point of view. In International Conference on Intelligent Computer Mathematics, pages 583-598. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85110-3_47.
  21. Makarius Wenzel. Interaction with formal mathematical documents in Isabelle/PIDE, 2019. URL: http://arxiv.org/abs/1905.01735.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact