Four decades of \textsc{Mizar}. Foreword
From MaRDI portal
Publication:286794
natural deductioncomputer proof assistantformalization of mathematicsMizarMizar mathematical library
Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Proceedings, conferences, collections, etc. pertaining to computer science (68-06) Mechanization of proofs and logical operations (03B35) Applications of set theory (03E75)
Recommendations
Cites work
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- scientific article; zbMATH DE number 3907807 (Why is no real title available?)
- scientific article; zbMATH DE number 1951637 (Why is no real title available?)
- scientific article; zbMATH DE number 1863397 (Why is no real title available?)
- A Brief Overview of Mizar
- A Declarative Language for the Coq Proof Assistant
- A comparison of Mizar and Isar
- A compendium of continuous lattices in MIZAR
- A synthesis of the procedural and declarative styles of interactive theorem proving
- ATP and presentation service for Mizar formalizations
- Automated Discovery of Properties of Rough Sets
- Commutative algebra in the Mizar system
- Flexary connectives in Mizar
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
- Licensing the Mizar Mathematical Library (MML)
- Mathematical Knowledge Management
- Mathematical knowledge management in MIZAR
- Methods of lemma extraction in natural deduction proofs
- New Developments in Parsing Mizar
- On equivalents of well-foundedness. An experiment in MIZAR
- On rewriting rules in Mizar
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- The Mizar Mathematical Library in OMDoc: translation and applications
- Types for Proofs and Programs
Cited in
(80)- Differentiation on interval
- Introduction to Diophantine approximation. II
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Extensions of orderings
- An integrated web platform for the Mizar Mathematical Library
- About graph unions and intersections
- Partial correctness of a Fibonacci algorithm
- Unification of graphs and relations in Mizar
- Elementary number theory problems. VIII
- Refined finiteness and degree properties in graphs
- Ordered rings and fields
- Underlying simple graphs
- An inference system of an extension of Floyd-Hoare logic for partial predicates
- On algebras of algorithms and specifications over uninterpreted data
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Partial correctness of GCD algorithm
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- About supergraphs. III
- Implicit function theorem. II
- Isomorphisms from the space of multilinear operators
- Natural addition of ordinals
- Aligning concepts across proof assistant libraries
- About graph complements
- Combining higher-order logic with set theory formalizations
- Concatenation of finite sequences
- Extended natural numbers and counters
- General theory and tools for proving algorithms in nominative data systems
- Partial correctness of an algorithm computing Lucas sequences
- Field extensions and Kronecker's construction
- Fundamental properties of fuzzy implications
- All Liouville numbers are transcendental
- Differentiability of polynomials over reals
- Embedded lattice and properties of Gram matrix
- Introduction to Liouville numbers
- Declarative Proof Translation (Short Paper)
- Eliminating models during model elimination
- Introduction to algebraic geometry
- On monomorphisms and subfields
- What's in a theorem name?
- Stability of the 7-3 compressor circuit for Wallace tree. I
- The role of the Mizar mathematical library for interactive proof development in Mizar
- About regular graphs
- Accessing the Mizar library with a weakly strict Mizar parser
- Enhancement of \textsc{Mizar} texts with transitivity property of predicates
- Formally real fields
- Implicit function theorem. I
- Diophantine sets. Preliminaries
- Fubini's theorem for non-negative or non-positive functions
- Introduction to stochastic finance: random variables and arbitrage theory
- Klein-Beltrami model. I
- Klein-Beltrami model. II
- On roots of polynomials and algebraically closed fields
- Invertible operators on Banach spaces
- From LCF to Isabelle/HOL
- Introduction to graph colorings
- Diophantine sets. II
- Formalization of the MRDP theorem in the Mizar system
- F. Riesz theorem
- Formal introduction to fuzzy implications
- Isomorphism theorem on vector spaces over a ring
- Integral of non positive functions
- Binary relations-based rough sets -- an automated approach
- Tarski geometry axioms. II
- Introduction to graph enumerations
- Semantics of Mizar as an Isabelle object logic
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- About graph mappings
- About vertex mappings
- Formal development of rough inclusion functions
- A simple example for linear partial differential equations and its solution using the method of separation of variables
- Continuity of multilinear operator on normed linear spaces
- Mizar: state-of-the-art and beyond
- About graph sums
- On an algorithmic algebra over simple-named complex-valued nominative data
- Introduction to stopping time in stochastic finance theory. II
- Automated Comparative Study of Some Generalized Rough Approximations
- Basic formal properties of triangular norms and conorms
- Fubini's theorem
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
This page was built for publication: Four decades of \textsc{Mizar}. Foreword
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286794)
