Tentative experiments with ellipsis in Mizar

DOI10.1007/978-3-642-31374-5_35zbMATH Open1360.68755OpenAlexW200592030MaRDI QIDQ2907348FDOQ2907348

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

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

Mathematics Subject Classification ID

Knowledge representation (68T30)

Cited In (9)

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

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)