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
Related Items
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
