Towards a Mizar Environment for Isabelle: Foundations and Language

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F16%3A00309757" target="_blank" >RIV/68407700:21730/16:00309757 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1145/2854065.2854070" target="_blank" >http://dx.doi.org/10.1145/2854065.2854070</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/2854065.2854070" target="_blank" >10.1145/2854065.2854070</a>

Result language

angličtina

Original language name

Towards a Mizar Environment for Isabelle: Foundations and Language

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

R - Projekt Ramcoveho programu EK

Publication year

2016

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

CPP 2016 Certified Proofs and Programs

ISBN

978-1-4503-4127-1

ISSN

—

e-ISSN

—

Number of pages

8

Pages from-to

58-65

Publisher name

ACM

Place of publication

New York

Event location

Saint Petersburg, FL

Event date

Jan 20, 2016

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000389021600008