Four decades of \textsc{Mizar}. Foreword
From MaRDI portal
Publication:286794
computer proof assistantformalization of mathematicsMizarMizar mathematical librarynatural deduction
Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Mechanization of proofs and logical operations (03B35) Applications of set theory (03E75) Proceedings, conferences, collections, etc. pertaining to computer science (68-06)
Recommendations
Cites work
- A Brief Overview of Mizar
- A comparison of Mizar and Isar
- A compendium of continuous lattices in MIZAR
- A Declarative Language for the Coq Proof Assistant
- 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
- 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?)
- 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
(93)- Aligning concepts across proof assistant libraries
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Isomorphism theorem on vector spaces over a ring
- F. Riesz theorem
- On roots of polynomials and algebraically closed fields
- Integral of non positive functions
- Formal introduction to fuzzy implications
- Formally real fields
- Introduction to stopping time in stochastic finance theory. II
- Implicit function theorem. I
- Introduction to Diophantine approximation. II
- Introduction to stochastic finance: random variables and arbitrage theory
- Klein-Beltrami model. I
- Klein-Beltrami model. II
- Fubini's theorem for non-negative or non-positive functions
- Diophantine sets. Preliminaries
- Refined finiteness and degree properties in graphs
- About graph unions and intersections
- Unification of graphs and relations in Mizar
- Partial correctness of a Fibonacci algorithm
- Eliminating models during model elimination
- About graph sums
- From LCF to Isabelle/HOL
- Field extensions and Kronecker's construction
- Underlying simple graphs
- About graph mappings
- About vertex mappings
- Formal development of rough inclusion functions
- On algebras of algorithms and specifications over uninterpreted data
- On an algorithmic algebra over simple-named complex-valued nominative data
- An inference system of an extension of Floyd-Hoare logic for partial predicates
- Partial correctness of GCD algorithm
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Fundamental properties of fuzzy implications
- Semantics of Mizar as an Isabelle object logic
- Isomorphisms from the space of multilinear operators
- Invertible operators on Banach spaces
- Implicit function theorem. II
- On monomorphisms and subfields
- Natural addition of ordinals
- About supergraphs. III
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- Diophantine sets. II
- Formalization of the MRDP theorem in the Mizar system
- Differentiability of polynomials over reals
- Introduction to Liouville numbers
- All Liouville numbers are transcendental
- Ordered rings and fields
- Embedded lattice and properties of Gram matrix
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Basic formal properties of triangular norms and conorms
- Concatenation of finite sequences
- 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
- Fubini's theorem
- About graph complements
- Stability of the 7-3 compressor circuit for Wallace tree. I
- Accessing the Mizar library with a weakly strict Mizar parser
- Enhancement of \textsc{Mizar} texts with transitivity property of predicates
- What's in a theorem name?
- Mizar: state-of-the-art and beyond
- Binary relations-based rough sets -- an automated approach
- Tarski geometry axioms. II
- Automated Comparative Study of Some Generalized Rough Approximations
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Declarative Proof Translation (Short Paper)
- Differentiation on interval
- Introduction to graph enumerations
- Introduction to algebraic geometry
- About regular graphs
- Elementary number theory problems. VIII
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- An integrated web platform for the Mizar Mathematical Library
- Combining higher-order logic with set theory formalizations
- Introduction to graph colorings
- Extensions of orderings
- Extended natural numbers and counters
- General theory and tools for proving algorithms in nominative data systems
- Partial correctness of an algorithm computing Lucas sequences
- Characterization of finite Galois extensions
- Formalization of separable version of Banach-Alaoglu theorem
- Triangular fuzzy set composed of two intersecting affine maps
- Higher order partial differentiable functions
- A formal proof of Stirling's formula
- Formalization of Wallis infinite product formula for and the Wallis integral
- Free product of groups
- Conway's normal form in the Mizar system
- Conway normal form: bridging approaches for comprehensive formalization of surreal numbers
- Some number relations
- About path and cycle graphs
- Formalization of orthogonal complements of normed spaces
- Elementary number theory problems. Part XIV: Diophantine equations
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)
