Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver

DOI10.1007/S10817-015-9332-6zbMATH Open1356.68197DBLPjournals/jar/Naumowicz15OpenAlexW2146945204WikidataQ59407645 ScholiaQ59407645MaRDI QIDQ286803FDOQ286803

Authors Adam Naumowicz 

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-015-9332-6

zbMATH Keywords

Boolean operationsMizarproof assistantsSAT solvers

Mathematics Subject Classification ID

Recommendations

• SAT-enhanced Mizar proof checking
• Theory and Applications of Satisfiability Testing
• Mechanical verification of SAT refutations with extended resolution
• Integrating a SAT solver with an LCF-style theorem prover
• Satisfiability checking: theory and applications

Cites Work

• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• A Brief Overview of Mizar
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• ATP and presentation service for Mizar formalizations
• An example of formalizing recent mathematical results in MIZAR
• Automated Discovery of Properties of Rough Sets
• Custom automations in Mizar
• Improving legibility of natural deduction proofs is not trivial
• 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
• 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
• SAT-enhanced Mizar proof checking
• Tentative experiments with ellipsis in Mizar

Cited In (10)

• Automated Improving of Proof Legibility in the Mizar System
• Computer certification of generalized rough sets based on relations
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Accessing the Mizar library with a weakly strict Mizar parser
• Flexary connectives in Mizar
• Logic2CNF
• SAT-enhanced Mizar proof checking
• Semantics of Mizar as an Isabelle object logic
• Automated Comparative Study of Some Generalized Rough Approximations
• MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers

Uses Software

• MiniSat
• Mizar

This page was built for publication: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver

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