Towards a Mizar Environment for Isabelle: Foundations and Language

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Towards a Mizar Environment for Isabelle: Foundations and Language

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Towards a Mizar Environment for Isabelle: Foundations and Language

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2016

Kód důvěrnosti údajů

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

Název statě ve sborníku

CPP 2016 Certified Proofs and Programs

ISBN

978-1-4503-4127-1

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

58-65

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

Saint Petersburg, FL

Datum konání akce

20. 1. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000389021600008