Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

Towards a mizar environment for isabelle: foundations and language

Towards a mizar environment for isabelle: foundations and language Towards a Mizar Environment for Isabelle: Foundations and Language Cezary Kaliszyk University of Innsbruck cezary.kaliszyk@uibk.ac.at Karol Pak University of Bialystok pakkarol@uwb.edu.pl Josef Urban Czech Technical University in Prague josef.urban@gmail.com 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. Categories and Subject Descriptors I.2.3 http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png

Towards a mizar environment for isabelle: foundations and language

Association for Computing Machinery — Jan 18, 2016

Loading next page...
/lp/association-for-computing-machinery/towards-a-mizar-environment-for-isabelle-foundations-and-language-6YEWNGz4AS

References

References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.

Datasource
Association for Computing Machinery
Copyright
Copyright © 2016 by ACM Inc.
ISBN
978-1-4503-4127-1
doi
10.1145/2854065.2854070
Publisher site
See Article on Publisher Site

Abstract

Towards a Mizar Environment for Isabelle: Foundations and Language Cezary Kaliszyk University of Innsbruck cezary.kaliszyk@uibk.ac.at Karol Pak University of Bialystok pakkarol@uwb.edu.pl Josef Urban Czech Technical University in Prague josef.urban@gmail.com 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. Categories and Subject Descriptors I.2.3

There are no references for this article.