Mechanizing complemented lattices within Mizar type system
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- A Brief Overview of Mizar
- A constructive algebraic hierarchy in Coq.
- ATP and presentation service for Mizar formalizations
- Automated Discovery of Properties of Rough Sets
- Boolean Algebra. A Correction
- Development of the theory of continuous lattices in MIZAR
- Improving legibility of natural deduction proofs is not trivial
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
- Isabelle/HOL. A proof assistant for higher-order logic
- Lattice Theory: Foundation
- Licensing the Mizar Mathematical Library (MML)
- Mathematical Knowledge Management
- Methods of lemma extraction in natural deduction proofs
- New Sets of Independent Postulates for the Algebra of Logic, With Special Reference to Whitehead and Russell's Principia Mathematica
- On rewriting rules in Mizar
- Prime filters and ideals in distributive lattices
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem
- Short single axioms for Boolean algebra
- Solution of the Robbins problem
Cited in
(18)- Stone lattices.
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Formalizing lattice-theoretical aspects of rough and fuzzy sets
- Pappus's hexagon theorem in real projective plane
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Automated Comparative Study of Some Generalized Rough Approximations
- Formalization of quasilattices
- Development of the theory of continuous lattices in MIZAR
- Accessing the Mizar library with a weakly strict Mizar parser
- Automatization of ternary Boolean algebras
- scientific article; zbMATH DE number 4072440 (Why is no real title available?)
- Pascal's theorem in real projective plane
- A compendium of continuous lattices in MIZAR
- Two axiomatizations of Nelson algebras.
- Binary relations-based rough sets -- an automated approach
- Tarski geometry axioms. II
- Computer certification of generalized rough sets based on relations
- On weakly associative lattices and near lattices
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)
