Automated Improving of Proof Legibility in the Mizar System

DOI10.1007/978-3-319-08434-3_27zbMath1304.68160OpenAlexW119865360MaRDI QIDQ5495936

Karol Pąk

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08434-3_27

zbMATH Keywords

SMT solversproof assistantslegibility of proofsoperations on languages

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items

The role of the Mizar mathematical library for interactive proof development in Mizar

Uses Software

• MizarMode
• Isabelle/Isar
• Isar
• Mizar
• z3
• PRocH

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Methods of lemma extraction in natural deduction proofs
• Tentative Experiments with Ellipsis in Mizar
• A Brief Overview of Mizar
• PRocH: Proof Reconstruction for HOL Light
• Mathematical Knowledge Management