SAT-Enhanced Mizar Proof Checking

DOI10.1007/978-3-319-08434-3_37zbMath1304.68159OpenAlexW731109MaRDI QIDQ5495946

Adam Naumowicz

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_37

zbMATH Keywords

Boolean operationsSATMizar

Mathematics Subject Classification ID

Related Items (5)

Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization ⋮ Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver ⋮ Mizar: State-of-the-art and Beyond ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Flexary connectives in Mizar

Uses Software

• Coq
• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• An example of formalizing recent mathematical results in MIZAR
• Methods of lemma extraction in natural deduction proofs
• ATP and presentation service for Mizar formalizations
• On rewriting rules in Mizar
• Custom automations in Mizar
• Tentative Experiments with Ellipsis in Mizar
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• A Brief Overview of Mizar
• Licensing the Mizar Mathematical Library
• Mathematical Knowledge Management
• Revisions as an Essential Tool to Maintain Mathematical Repositories
• Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking

This page was built for publication: SAT-Enhanced Mizar Proof Checking