Tentative experiments with ellipsis in Mizar

DOI10.1007/978-3-642-31374-5_35MaRDI QIDQ2907348zbMATH OpenOpenAlexFDO

Authors Artur Korniłowicz

Publication date 7 September 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-31374-5_35

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• scientific article; zbMATH DE number 1405440
• Flexary connectives in Mizar
• Using and parsing the Mizar language
• A Brief Overview of Mizar
• Custom automations in Mizar

Cited in

(9)

• Flexary connectives in Mizar
• Methods of lemma extraction in natural deduction proofs
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• Readable formalization of Euler's partition theorem in Mizar
• Flexary operators for formalized mathematics
• Automated Improving of Proof Legibility in the Mizar System
• SAT-enhanced Mizar proof checking

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Tentative experiments with ellipsis in Mizar

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