Interaction with formal mathematical documents in Isabelle/PIDE

DOI10.1007/978-3-030-23250-4_1zbMath1428.68347arXiv1905.01735OpenAlexW2965911323MaRDI QIDQ2287890

Makarius Wenzel

Publication date: 22 January 2020

Full work available at URL: https://arxiv.org/abs/1905.01735

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Unnamed Item, Unnamed Item, From LCF to Isabelle/HOL, The Isabelle/Naproche natural language proof assistant, Integration of formal proof into unified assurance cases with Isabelle/SACM

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/Isar
• Proof General
• PIDE
• Isabelle/jEdit
• Sledgehammer
• Isabelle/PIDE
• Archive Formal Proofs