Declarative Proof Translation (Short Paper)

DOI10.4230/LIPICS.ITP.2019.35MaRDI QIDQ5875449zbMATH OpenOpenAlexFDO

Authors Cezary Kaliszyk, Karol Pąk

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPIcs.ITP.2019.35

zbMATH Keywords

declarative proofIsabelle/IsarMizartranslation

Mathematics Subject Classification ID

Cites work

• A comparison of Mizar and Isar
• A Declarative Language for the Coq Proof Assistant
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Four decades of \textsc{Mizar}. Foreword
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• Isabelle import infrastructure for the Mizar Mathematical Library
• Proof auditing formalised mathematics
• Semantics of Mizar as an Isabelle object logic
• The Lean theorem prover (system description)
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(3)

• Translating between implicit and explicit versions of proof
• Declarative representation of proof terms
• Combining higher-order logic with set theory formalizations

Describes a project that uses

Uses Software

• Coq
• Isar
• Mizar
• Lean
• miz3

This page was built for publication: Declarative Proof Translation (Short Paper)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875449)