A compendium of continuous lattices in MIZAR

DOI10.1023/A:1021966832558zbMath1064.68082OpenAlexW1585415359MaRDI QIDQ1868506

Piotr Rudnicki, Grzegorz Bancerek

Publication date: 27 April 2003

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1021966832558

zbMATH Keywords

set theoryformalization of mathematicsproof checkingmathematical knowledge managementMIZARQED projecttheory of continuous lattices

Mathematics Subject Classification ID

Related Items (15)

Four decades of {\textsc{Mizar}}. Foreword ⋮ Mizar: State-of-the-art and Beyond ⋮ Formalizing Physics: Automation, Presentation and Foundation Issues ⋮ An example of formalizing recent mathematical results in MIZAR ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Formalising Mathematics in Simple Type Theory ⋮ The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF ⋮ Combining higher-order logic with set theory formalizations ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Flexary connectives in Mizar ⋮ On the Structure of Mizar Types ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Formalizing Arrow's theorem ⋮ Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description

Uses Software

• Mizar
• Automath

This page was built for publication: A compendium of continuous lattices in MIZAR