Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
From MaRDI portal
Publication:286803
DOI10.1007/s10817-015-9332-6zbMath1356.68197OpenAlexW2146945204WikidataQ59407645 ScholiaQ59407645MaRDI QIDQ286803
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Computer Certification of Generalized Rough Sets Based on Relations ⋮ Flexary connectives in Mizar ⋮ Automated Comparative Study of Some Generalized Rough Approximations ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Logic2CNF ⋮ Semantics of Mizar as an Isabelle object logic
Uses Software
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
- Improving legibility of natural deduction proofs is not trivial
- 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
- Automated Discovery of Properties of Rough Sets
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- SAT-Enhanced Mizar Proof Checking
- Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
- Mathematical Knowledge Management
This page was built for publication: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
