Four decades of \textsc{Mizar}. Foreword
From MaRDI portal
Publication:286794
DOI10.1007/S10817-015-9345-1zbMATH Open1336.00111OpenAlexW2184838578WikidataQ59407702 ScholiaQ59407702MaRDI QIDQ286794FDOQ286794
Authors:
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-9345-1
Recommendations
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)
Cites Work
- Title not available (Why is that?)
- A Brief Overview of Mizar
- A synthesis of the procedural and declarative styles of interactive theorem proving
- The Mizar Mathematical Library in OMDoc: translation and applications
- Flexary connectives in Mizar
- A compendium of continuous lattices in MIZAR
- A comparison of Mizar and Isar
- Methods of lemma extraction in natural deduction proofs
- ATP and presentation service for Mizar formalizations
- On rewriting rules in Mizar
- On equivalents of well-foundedness. An experiment in MIZAR
- Mathematical knowledge management in MIZAR
- New Developments in Parsing Mizar
- A Declarative Language for the Coq Proof Assistant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Licensing the Mizar Mathematical Library (MML)
- Automated Discovery of Properties of Rough Sets
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Types for Proofs and Programs
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
- Mathematical Knowledge Management
- Commutative algebra in the Mizar system
Cited In (80)
- Introduction to Diophantine approximation. II
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- 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
- 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
- Concatenation of finite sequences
- Field extensions and Kronecker's construction
- Fundamental properties of fuzzy implications
- Eliminating models during model elimination
- On monomorphisms and subfields
- What's in a theorem name?
- About regular graphs
- The role of the Mizar mathematical library for interactive proof development in Mizar
- 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
- 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
- Semantics of Mizar as an Isabelle object logic
- About graph mappings
- About vertex mappings
- Formal development of rough inclusion functions
- 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
- Basic formal properties of triangular norms and conorms
- Fubini's theorem
- Extensions of orderings
- Elementary number theory problems. VIII
- Combining higher-order logic with set theory formalizations
- Extended natural numbers and counters
- General theory and tools for proving algorithms in nominative data systems
- Partial correctness of an algorithm computing Lucas sequences
- Declarative Proof Translation (Short Paper)
- All Liouville numbers are transcendental
- Differentiability of polynomials over reals
- Embedded lattice and properties of Gram matrix
- Introduction to Liouville numbers
- Introduction to algebraic geometry
- Stability of the 7-3 compressor circuit for Wallace tree. I
- Introduction to graph colorings
- Introduction to graph enumerations
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- 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
- Automated Comparative Study of Some Generalized Rough Approximations
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- Differentiation on interval
Uses Software
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)
