\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

I/Mizar

Table of Contents

1. Introduction

Kaliszyk and Pak have implemented Mizar as an "object logic" in Isabelle, which is intriguing. They have published several iterations of this, and their latest one (in 2019) is the most sophisticated. Particularly intriguing is how they present their encoding to work "atop" some foundations (again, encoded in Isabelle; so we could have I/Mizar work atop of I/HOL or I/FOL [or I/*]).

2. References

  • Cezary Kaliszyk and Karol Pąk,
    "Semantics of Mizar as an Isabelle Object Logic".
    Journal of Automated Reasoning 63 (2019) pp.557–595 doi:10.1007/s10817-018-9479-z.

Last Updated 2022-07-19 Tue 10:21.