Mechanizing complemented lattices within Mizar type system
From MaRDI portal
Publication:286797
DOI10.1007/S10817-015-9333-5zbMATH Open1356.68189DBLPjournals/jar/Grabowski15OpenAlexW2128085487WikidataQ59407587 ScholiaQ59407587MaRDI QIDQ286797FDOQ286797
Authors: Adam Grabowski 
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-9333-5
Recommendations
Mechanization of proofs and logical operations (03B35) Complemented lattices, orthocomplemented lattices and posets (06C15)
Cites Work
- Title not available (Why is that?)
- A Brief Overview of Mizar
- Isabelle/HOL. A proof assistant for higher-order logic
- Lattice Theory: Foundation
- Prime filters and ideals in distributive lattices
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- Solution of the Robbins problem
- A constructive algebraic hierarchy in Coq.
- Short single axioms for Boolean algebra
- Methods of lemma extraction in natural deduction proofs
- ATP and presentation service for Mizar formalizations
- On rewriting rules in Mizar
- Development of the theory of continuous lattices in MIZAR
- Improving legibility of natural deduction proofs is not trivial
- New Sets of Independent Postulates for the Algebra of Logic, With Special Reference to Whitehead and Russell's Principia Mathematica
- Boolean Algebra. A Correction
- 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
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
Cited In (18)
- Formalization of quasilattices
- Stone lattices.
- Pappus's hexagon theorem in real projective plane
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Two axiomatizations of Nelson algebras.
- Title not available (Why is that?)
- Computer certification of generalized rough sets based on relations
- The role of the Mizar mathematical library for interactive proof development in Mizar
- On weakly associative lattices and near lattices
- Accessing the Mizar library with a weakly strict Mizar parser
- A compendium of continuous lattices in MIZAR
- Formalizing lattice-theoretical aspects of rough and fuzzy sets
- Automatization of ternary Boolean algebras
- Pascal's theorem in real projective plane
- Binary relations-based rough sets -- an automated approach
- Tarski geometry axioms. II
- Development of the theory of continuous lattices in MIZAR
- Automated Comparative Study of Some Generalized Rough Approximations
Uses Software
This page was built for publication: Mechanizing complemented lattices within Mizar type system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286797)
