Access the full text.
Sign up today, get an introductory month for just $19.
A. Grzegorczyk (1971)
Zarys arytmetyki teoretycznej
P. Rudnicki, A. Trybulec (1999)
On Equivalents of Well-FoundednessJournal of Automated Reasoning, 23
Jacques Fleuriot, Lawrence Paulson (1998)
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia
(1955)
General Topology. van Nostrand
A. Y. Shibakov, A. Trybulec (1996)
The Cantor setFormalized Mathematics, 5
Beata Padlewska, Agata Darmochwa (1990)
Topological Spaces and Continuous Functions
G. Bancerek (2001)
Development of the theory of continuous lattices in Mizar
G. Bancerek (1998)
Arithmetic of Non-Negative Rational Numbers 1
G. Bancerek (1998)
The Lawson Topology 1
Adam Grabowski, R. Milewski (1997)
Boolean Posets, Posets under Inclusion and Products of Relational Structures 1
A. Trybulec (1997)
Scott topologyFormalized Mathematics, 6
The formalization of Chapter IV of the ccl-book has begun recently and so far pp. 179–183, items 1.1–1.12 have been covered by G
G. Bancerek (1990)
Tarski's Classes and Ranks
Józef Bia (1990)
Group and Field Definitions
G. Bancerek (1998)
Lawson topology in continuous latticesFormalized Mathematics, 7
J. Gryko (1998)
Injective spacesFormalized Mathematics, 7
(1990)
Built-in concepts, Formalized Mathematics
(2001)
Mathematical knowledge management in MIZAR
van Jutting (1994)
Checking Landau's “Grundlagen” in the Automath System: Parts of Chapter 3 (Verification)Studies in logic and the foundations of mathematics, 133
P. Rudnicki (1998)
Kernel Projections and Quotient Lattices
Czeslaw Bylinski (2004)
Some Basic Properties of Sets
E. Landau (1934)
Grundlagen der AnalysisThe Modern Language Journal, 45
S. Ja´skowski (1934)
On the Rules of Supposition in Formal Logic
(2001)
FOM: 107: Automated proof checking
Freek Wiedijk (2000)
The De Bruijn Factor
(2001)
Duality based on the Galois connection
G. Bancerek (1997)
Directed Sets, Nets, Ideals, Filters, and Maps 1
A. Trybulec (1996)
Functors for Alternative Categories
G. Bancerek (1990)
Konig's Theorem
Lawrence Paulson, Krzysztof Grabczewski (1996)
Mechanizing set theoryJournal of Automated Reasoning, 17
H. Herrlich, M. Husek (1985)
Galois Connections
Freek Wiedijk (1999)
Mizar : An Impression
A Primer of Complete Lattices pages items article author(s)
A. Degtyarev, Alexander Lyaletski, M. Morokhovets (1999)
Evidence Algorithm and Sequent Logical Inference Search
G. Bancerek (1997)
Duality in relation structuresFormalized Mathematics, 6
A. Trybulec (1990)
Built-in conceptsFormalized Mathematics, 1
Non Negative Real Numbers, Part I
G. Bancerek (1991)
Complete latticesFormalized Mathematics, 2
S. Żukowski (1990)
Introduction to Lattice Theory
C. Byli´nski (1991)
Category ensFormalized Mathematics, 2
Rp Nederpelt, J. Geuvers, R. Vrijer, L. Jutting, D. Daalen (1994)
Selected papers on AutomathStudies in logic and the foundations of mathematics, 133
T. Nipkow (1996)
Winskel is (almost) Right: Towards a Mechanized Semantics TextbookFormal Aspects of Computing, 10
G. Bancerek (2001)
Categorial background for duality theoryFormalized Mathematics, 9
A. Trybulec (1996)
Categories without Uniqueness of cod and dom
Martin Davis (1981)
Obvious Logical Inferences
(1939)
On the Rules of Supposition in Formal Logic, Studia Logica, Warsaw University, 1934
R. Milewski
Algebraic Lattices
(1997)
Prime ideals and filters
A. Korniłowicz (1997)
On the topological properties of meet-continuous latticesFormalized Mathematics, 6
G. Gierz, K. Hofmann, K. Keimel, J. Lawson, M. Mislove, D. Scott (2003)
Continuous Lattices and Domains: The Scott Topology
A. Trybulec (1990)
Tarski Grothendieck Set Theory
Wojciech Trybulec (1990)
Partially Ordered Sets
Artur Kornii
Journal of Formalized Mathematics on the Topological Properties of Meet-continuous Lattices
G. Gierz, K. Hofmann, K. Keimel, J. Lawson, M. Mislove, D. Scott (1980)
A Compendium of Continuous Lattices
Artur Korniłowicz (1996)
Cartesian Products of Relations and Relational Structures 1
L. C. Paulson, Grabczewski (1996)
Mechanizing set theory: Cardinal arithmetic and the axiom of choiceJ. Automated Reasoning, 17
Czesław Bylí (1989)
Introduction to Categories and Functors
(1998)
Bases and refinements of topologies
(1990)
An Introduction to PC Mizar Fondation Philippe le Hodey
(1982)
Stone Spaces
Edmund Woronowicz, Anna Zalewska (1990)
Properties of Binary Relations
(1994)
and R
G. Bancerek (1991)
Cartesian Product of Functions
Zinaida Trybulec (1990)
Boolean Properties of Sets
H. Rasiowa, R. Sikorski (1963)
The mathematics of metamathematics
Estimating the cost of a standard library for a mathematical proof checker
G. Bancerek, N. Endou, Y. Shidama (2002)
Lim-inf Convergence and its Compactness
G. Bancerek (1997)
Bounds in Posets and Relational Substructures 1
G. Szász, B. Balkay, G. Tóth (1965)
Introduction to lattice theoryAmerican Mathematical Monthly, 72
A. Trybulec (1997)
Moore–Smith convergenceFormalized Mathematics, 6
B. Madras (2004)
Product of Family of Universal Algebras
P. Rudnicki (1987)
Obvious inferencesJournal of Automated Reasoning, 3
G. Bancerek (1996)
The \way-below" Relation
P. Rudnicki, Christoph Schwarzweller, A. Trybulec (2001)
Commutative Algebra in the Mizar SystemJ. Symb. Comput., 32
G. Bancerek (1999)
Continuous Lattices of Maps between T 0 Spaces 1
Edmund Woronowicz (1990)
Relations Defined on Sets
This paper reports on the MIZAR formalization of the theory of continuous lattices as presented in Gierz et al.: A Compendium of Continuous Lattices, 1980. By a MIZAR formalization we mean a formulation of theorems, definitions, and proofs written in the MIZAR language whose correctness is verified by the MIZAR processor. This effort was originally motivated by the question of whether or not the MIZAR system was sufficiently developed for the task of expressing advanced mathematics. The current state of the formalization – 57 MIZAR articles written by 16 authors – indicates that in principle the MIZAR system has successfully met the challenge. To our knowledge it is the most sizable effort aimed at mechanically checking some substantial and relatively recent field of advanced mathematics. However, it does not mean that doing mathematics in MIZAR is as simple as doing mathematics traditionally (if doing mathematics is simple at all). The work of formalizing the material of the Gierz et al. compendium has (i) prompted many improvements of the MIZAR proof checking system, (ii) caused numerous revisions of the the MIZAR data base, and (iii) contributed to the “to do” list of further changes to the MIZAR system.
Journal of Automated Reasoning – Springer Journals
Published: Sep 30, 2004
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get an introductory month for just $19.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.