research-article

Open access

Towards a Mizar environment for Isabelle: foundations and language

Authors:

Cezary Kaliszyk,

Josef UrbanAuthors Info & Claims

CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs

Pages 58 - 65

https://doi.org/10.1145/2854065.2854070

Published: 18 January 2016 Publication History

Abstract

In this paper we explore the possibility of emulating the Mizar environment as close as possible inside the Isabelle logical framework. We introduce adaptations to the Isabelle/FOL object logic that correspond to the logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how Isabelle types can be used to differentiate between the syntactic categories of the Mizar language, such as sets and Mizar types including modes and attributes, and show how they interact with the basic constructs of the Tarski-Grothendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Isabelle/Pure language elements for introducing definitions and theorems. We finally consider the definite and indefinite description operators in Mizar and their use to introduce definitions by “means” and “equals”. We demonstrate the usability of the environment on a sample Mizar-style formalization, with cluster inferences and “by” steps performed manually.

References

[1]

S. Agerholm and M. J. C. Gordon. Experiments with ZF set theory in HOL and isabelle. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, volume 971 of Lecture Notes in Computer Science, pages 32–45. Springer, 1995.

Digital Library

[2]

G. Bancerek and P. Rudnicki. A Compendium of Continuous Lattices in MIZAR. J. Autom. Reasoning, 29(3-4):189–224, 2002.

Digital Library

[3]

M. Davis. Obvious logical inferences. In P. J. Hayes, editor, IJCAI, pages 530–531. William Kaufmann, 1981.

Digital Library

[4]

F. Haftmann and T. Nipkow. Code generation via higher-order rewrite systems. In M. Blume, N. Kobayashi, and G. Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, volume 6009 of Lecture Notes in Computer Science, pages 103–117. Springer, 2010.

Digital Library

[5]

J. Harrison. A Mizar mode for HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, volume 1125 of Lecture Notes in Computer Science, pages 203–220, Turku, Finland, 1996. Springer-Verlag.

Digital Library

[6]

J. Hurd. The OpenTheory standard theory library. In M. G. Bobaru, K. Havelund, G. J. Holzmann, and R. Joshi, editors, NASA Formal Methods, volume 6617 of LNCS, pages 177–191. Springer, 2011.

Digital Library

[7]

M. Iancu, M. Kohlhase, F. Rabe, and J. Urban. The Mizar mathematical library in OMDoc: Translation and applications. J. Autom. Reasoning, 50(2):191–202, 2013.

Digital Library

[8]

S. Jaśkowski. On the rules of suppositions. Studia Logica, 1, 1934.

[9]

C. Kaliszyk and A. Krauss. Scalable LCF-style proof translation. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), volume 7998 of LNCS, pages 51–66. Springer, 2013.

Digital Library

[10]

C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 2015.

Digital Library

[11]

A. Krauss and A. Schropp. A mechanized translation from higherorder logic to set theory. In M. Kaufmann and L. C. Paulson, editors, Interactive Theorem Proving (ITP 2010), volume 6172 of LNCS, pages 323–338. Springer, 2010.

Digital Library

[12]

O. Kunˇcar. Reconstruction of the Mizar type system in the HOL Light system. In J. Pavlu and J. Safrankova, editors, WDS Proceedings of Contributed Papers: Part I – Mathematics and Computer Sciences, pages 7–12. Matfyzpress, 2010.

[13]

R. Matuszewski and P. Rudnicki. Mizar: the first 30 years. Mechanized Mathematics and Its Applications, 4:3–24, 2005.

[14]

S. Merz. Mechanizing TLA in Isabelle. In R. Rodošek, editor, Workshop on Verification in New Orientations, pages 54–74, Maribor, July 1995. Univ. of Maribor.

[15]

A. Naumowicz. Enhanced Processing of Adjectives in Mizar. In A. Grabowski and A. Naumowicz, editors, Computer Reconstruction of the Body of Mathematics, volume 18(31) of Studies in Logic, Grammar and Rhetoric, pages 89–101. University of Białystok, 2009.

[16]

S. Obua. Partizan games in Isabelle/HOLZF. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, Third International Colloquium, volume 4281 of Lecture Notes in Computer Science, pages 272–286. Springer, 2006.

Digital Library

[17]

S. Obua, J. D. Fleuriot, P. Scott, and D. Aspinall. Type inference for ZFH. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM, volume 9150 of Lecture Notes in Computer Science, pages 87– 101. Springer, 2015.

[18]

L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science (1990), pages 361–386, 1990.

[19]

L. C. Paulson. Set theory for verification: I. From foundations to functions. J. Autom. Reasoning, 11(3):353–389, 1993.

Digital Library

[20]

L. C. Paulson and J. C. Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In G. Sutcliffe, S. Schulz, and E. Ternovska, editors, The 8th International Workshop on the Implementation of Logics, IWIL 2010, volume 2 of EPiC Series, pages 1–11. EasyChair, 2010.

[21]

F. J. Pelletier. A brief history of natural deduction. History and Philosophy of Logic, 20:1 – 31, 1999.

[22]

qed. The QED Manifesto. In A. Bundy, editor, International Conference on Automated Deduction (CADE 1994), volume 814 of LNCS, pages 238–251. Springer, 1994.

Digital Library

[23]

F. Rabe. A logical framework combining model and proof theory. Mathematical Structures in Computer Science, 23(5): 945–1001, 2013.

[24]

. URL http://dx.doi.org/10.1017/ S0960129512000424.

[25]

P. Rudnicki. Obvious Inferences. J. Autom. Reasoning, 3(4):383–393, 1987.

Digital Library

[26]

S. Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3): 111–126, 2002.

Digital Library

[27]

C. Schürmann. The twelf proof assistant. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 79–83. Springer, 2009.

Digital Library

[28]

A. Tarski. Über unerreichbare Kardinalzahlen. Fundamenta Mathematica, 30:68–89, 1938. URL http://matwbn.icm.edu.pl/ ksiazki/fm/fm30/fm30113.pdf.

[29]

J. Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools, 15 (1):109–130, 2006.

[30]

J. Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006.

Digital Library

[31]

J. Urban and G. Sutcliffe. Atp-based cross-verification of Mizar proofs: Method, systems, and first experiments. Mathematics in Computer Science, 2(2):231–251, 2008. URL http://dx.doi.org/ 10.1007/s11786-008-0053-7.

[32]

M. Wenzel. Isar - A generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, pages 167–184. Springer, 1999.

Digital Library

[33]

M. Wenzel. The Isabelle/Isar reference manual, 2015.

[34]

M. Wenzel, L. C. Paulson, and T. Nipkow. The Isabelle framework. In O. A. Mohamed, C. A. Muñoz, and S. Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, volume 5170 of Lecture Notes in Computer Science, pages 33– 38. Springer, 2008.

Digital Library

[35]

F. Wiedijk. CHECKER - notes on the basic inference step in Mizar. available at http://www.cs.kun.nl/∼freek/mizar/by.dvi, 2000. URL http://www.cs.kun.nl/~freek/mizar/by.dvi.

Cited By

Kaliszyk CPąk K(2023)Combining Higher-Order Logic with Set Theory FormalizationsJournal of Automated Reasoning10.1007/s10817-023-09663-567:2Online publication date: 25-May-2023
https://doi.org/10.1007/s10817-023-09663-5
The mathlib Community Blanchette JHriţcu C(2020)The lean mathematical libraryProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373824(367-381)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373824
Naumowicz A(2020)An Experiment on Mizar Adjectives with Extra Visible Arguments2020 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)10.1109/SYNASC51798.2020.00026(97-100)Online publication date: Sep-2020
https://doi.org/10.1109/SYNASC51798.2020.00026
Show More Cited By

Index Terms

Towards a Mizar environment for Isabelle: foundations and language
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
  2. Models of computation
    1. Computability

Recommendations

Flexary connectives in Mizar

One of the main components of the Mizar project is the Mizar language, a computer language invented to reflect the natural language of mathematics. From the very beginning various linguistic constructions and grammar rules which enable us to write texts ...
Programming and verifying a declarative first-order prover in Isabelle/HOL

We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
A Formalization and Proof Checker for Isabelle’s Metalogic
Abstract
Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2016: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs

January 2016

196 pages

ISBN:9781450341271

DOI:10.1145/2854065

Program Chairs:
Jeremy Avigad
Carnegie Mellon University, USA
,
Adam Chlipala
MIT, USA

Copyright © 2016 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 January 2016

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Austrian Science Fund

Conference

CPP 2016

Sponsor:

SIGPLAN

CPP 2016: Certified Proofs and Programs

January 18 - 19, 2016

FL, St. Petersburg, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
491
Total Downloads

Downloads (Last 12 months)79
Downloads (Last 6 weeks)14

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kaliszyk CPąk K(2023)Combining Higher-Order Logic with Set Theory FormalizationsJournal of Automated Reasoning10.1007/s10817-023-09663-567:2Online publication date: 25-May-2023
https://doi.org/10.1007/s10817-023-09663-5
The mathlib Community Blanchette JHriţcu C(2020)The lean mathematical libraryProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373824(367-381)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373824
Naumowicz A(2020)An Experiment on Mizar Adjectives with Extra Visible Arguments2020 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)10.1109/SYNASC51798.2020.00026(97-100)Online publication date: Sep-2020
https://doi.org/10.1109/SYNASC51798.2020.00026
Lu BCao RLu YLuo X(2019)Design and Formal Analysis of an Authentication Protocol, eWMDP on Wearable DevicesIEEE Access10.1109/ACCESS.2019.29277727(97771-97783)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2927772
Zhan B(2019)Formalization of the Fundamental Group in Untyped Set Theory Using Auto2Journal of Automated Reasoning10.1007/s10817-018-9478-063:2(517-538)Online publication date: 2-Aug-2019
https://dl.acm.org/doi/10.1007/s10817-018-9478-0
Kaliszyk CPąk K(2018)Semantics of Mizar as an Isabelle Object LogicJournal of Automated Reasoning10.1007/s10817-018-9479-zOnline publication date: 28-Aug-2018
https://doi.org/10.1007/s10817-018-9479-z
Bancerek GByliński CGrabowski AKorniłowicz AMatuszewski RNaumowicz APąk K(2018)The Role of the Mizar Mathematical Library for Interactive Proof Development in MizarJournal of Automated Reasoning10.1007/s10817-017-9440-661:1-4(9-32)Online publication date: 1-Jun-2018
https://dl.acm.org/doi/10.1007/s10817-017-9440-6
Betzendahl JKohlhase M(2018)Translating the IMPS Theory Library to MMT/OMDocIntelligent Computer Mathematics10.1007/978-3-319-96812-4_2(7-22)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96812-4_2
Kaliszyk CPąk K(2018)Isabelle Import Infrastructure for the Mizar Mathematical LibraryIntelligent Computer Mathematics10.1007/978-3-319-96812-4_13(131-146)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96812-4_13
Kaliszyk CPąk K(2017)Isabelle Formalization of Set Theoretic Structures and Set ComprehensionsMathematical Aspects of Computer and Information Sciences10.1007/978-3-319-72453-9_12(163-178)Online publication date: 21-Dec-2017
https://doi.org/10.1007/978-3-319-72453-9_12
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents