Abstract: |
In their article titled From Types to Sets by Local Type
Definitions in Higher-Order Logic and published in the
proceedings of the conference Interactive Theorem
Proving in 2016, Ondřej Kunčar and Andrei Popescu propose an
extension of the logic Isabelle/HOL and an associated algorithm for
the relativization of the type-based theorems to
more flexible set-based theorems, collectively
referred to as Types-To-Sets. One of the aims of
their work was to open an opportunity for the development of a
software tool for applied relativization in the implementation of the
logic Isabelle/HOL of the proof assistant Isabelle. In this article,
we provide a prototype of a software framework for the interactive
automated relativization of theorems in Isabelle/HOL, developed as an
extension of the proof language Isabelle/Isar. The software framework
incorporates the implementation of the proposed extension of the
logic, and builds upon some of the ideas for further work expressed in
the original article on Types-To-Sets by Ondřej Kunčar and Andrei
Popescu and the subsequent article Smooth Manifolds and Types
to Sets for Linear Algebra in Isabelle/HOL that was written
by Fabian Immler and Bohua Zhan and published in the proceedings of
the International Conference on Certified Programs and
Proofs in 2019. |
BibTeX: |
@article{Types_To_Sets_Extension-AFP,
author = {Mihails Milehins},
title = {Extension of Types-To-Sets},
journal = {Archive of Formal Proofs},
month = sep,
year = 2021,
note = {\url{https://isa-afp.org/entries/Types_To_Sets_Extension.html},
Formal proof development},
ISSN = {2150-914x},
}
|