CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

The Isabelle/Isar language has been heavily inspired by the Mizar style, however already from the beginning it has been different in many ways and it has been evolving in different directions than the syntax the Mizar language. These differences were mostly motivated by the particular needs of integration with Isabelle at a particular time, in particular in order to make various proof tactics and other techniques associated with the LCF style available.

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 meta-logic of Mizar, as well as Isar inner syntax notations that correspond to these of the Mizar language. We show how meta-level types can be used to differenciate 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-Groethendieck set theory. We discuss Mizar definitions and provide simple abbreviations that allow the introduction of Mizar predicates, functions, attributes and modes using the Pure definition syntax. 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.

Mon 18 Jan
Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change

14:00 - 15:30: CPP - Session 3: Design and Implementation of Theorem Provers at Room St Petersburg II
CPP-2016-main14:00 - 14:30
Evgenii KotelnikovChalmers University of Technology, Laura KovacsChalmers University of Technology, Giles RegerUniversity of Manchester, Andrei VoronkovUniversity of Manchester
CPP-2016-main14:30 - 15:00
Lukasz CzajkaUniversity of Innsbruck
CPP-2016-main15:00 - 15:30
Cezary KaliszykUniversity of Innsbruck, Karol PąkUniversity of Bialystok, Institute of Computer Science, Josef Urban