SAT-enhanced Mizar proof checking
From MaRDI portal
Recommendations
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- Mechanical verification of SAT refutations with extended resolution
- Automated Improving of Proof Legibility in the Mizar System
- Efficient, verified checking of propositional proofs
- Presenting and explaining Mizar
Cites work
- A Brief Overview of Mizar
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- An example of formalizing recent mathematical results in MIZAR
- ATP and presentation service for Mizar formalizations
- Custom automations in Mizar
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- Integrating a SAT solver with an LCF-style theorem prover
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
- Licensing the Mizar Mathematical Library (MML)
- Mathematical Knowledge Management
- Methods of lemma extraction in natural deduction proofs
- MizAR 40 for Mizar 40
- On rewriting rules in Mizar
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Tentative experiments with ellipsis in Mizar
Cited in
(5)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Flexary connectives in Mizar
- 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
This page was built for publication: SAT-enhanced Mizar proof checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5495946)
