Mechanizing complemented lattices within Mizar type system

DOI10.1007/S10817-015-9333-5zbMath1356.68189OpenAlexW2128085487WikidataQ59407587 ScholiaQ59407587MaRDI QIDQ286797

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

zbMATH Keywords

formalization of mathematicsMizarcomplemented lattices

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complemented lattices, orthocomplemented lattices and posets (06C15)

Related Items (15)

Pappus's hexagon theorem in real projective plane ⋮ On weakly associative lattices and near lattices ⋮ Stone lattices. ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Computer Certification of Generalized Rough Sets Based on Relations ⋮ Automatization of ternary Boolean algebras ⋮ Pascal's theorem in real projective plane ⋮ Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets ⋮ Two axiomatizations of Nelson algebras. ⋮ Binary relations-based rough sets -- an automated approach ⋮ Tarski geometry axioms. II ⋮ Automated Comparative Study of Some Generalized Rough Approximations ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ On two alternative axiomatizations of lattices by McKenzie and Sholander ⋮ Formalization of quasilattices

Uses Software

• Mizar
• Unnamed Item
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• 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.
• Isabelle/HOL. A proof assistant for higher-order logic
• 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
• Improving legibility of natural deduction proofs is not trivial
• Lattice Theory: Foundation
• A Brief Overview of Mizar
• 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
• 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 M<scp>izar</scp>proof checking

This page was built for publication: Mechanizing complemented lattices within Mizar type system