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

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

zbMATH Keywords

Boolean operationsMizarproof assistantsSAT solvers

Mathematics Subject Classification ID

Cites Work

• MizAR 40 for Mizar 40
• Title not available (Why is that?)
• A Brief Overview of 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
• Integrating a SAT solver with an LCF-style theorem prover
• 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
• Licensing the Mizar Mathematical Library (MML)
• 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 Mizar proof checking
• Mathematical Knowledge Management
• An example of formalizing recent mathematical results in MIZAR

Cited In (8)

• Automated Improving of Proof Legibility in the Mizar System
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Flexary connectives in Mizar
• Logic2CNF
• Accessing the Mizar Library with a Weakly Strict Mizar Parser
• Semantics of Mizar as an Isabelle object logic
• Automated Comparative Study of Some Generalized Rough Approximations
• Computer Certification of Generalized Rough Sets Based on Relations

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)