The role of the Mizar mathematical library for interactive proof development in Mizar
From MaRDI portal
Publication:1663215
DOI10.1007/S10817-017-9440-6zbMATH Open1433.68530OpenAlexW2770430340WikidataQ59610101 ScholiaQ59610101MaRDI QIDQ1663215FDOQ1663215
Grzegorz Bancerek, Adam Naumowicz, Czesław Byliński, Adam Grabowski, Roman Matuszewski, Artur Korniłowicz, Karol Pąk
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9440-6
Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Mathematical knowledge management (68V30)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- MizAR 40 for Mizar 40
- Mizar: State-of-the-art and Beyond
- Tools for MML Environment Analysis
- MPTP-motivation, implementation, first experiments
- MPTP 0.2: Design, implementation, and initial experiments
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- Mining the Archive of Formal Proofs
- The Mizar Mathematical Library in OMDoc: translation and applications
- Continuous Lattices and Domains
- Mechanizing complemented lattices within Mizar type system
- Flexary connectives in Mizar
- A compendium of continuous lattices in MIZAR
- Methods of lemma extraction in natural deduction proofs
- ATP and presentation service for Mizar formalizations
- On rewriting rules in Mizar
- Mathematical knowledge management in MIZAR
- Four decades of {\textsc{Mizar}}. Foreword
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
- Lemmatization for Stronger Reasoning in Large Theories
- Licensing the Mizar Mathematical Library
- Mathematical Knowledge Management
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- SAT-Enhanced Mizar Proof Checking
- Information Retrieval and Rendering with MML Query
- Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
- Mathematical Knowledge Management
- Glushkov's evidence algorithm
- On Better-Quasi-Ordering Countable Series-Parallel Orders
- A Machine-Checked Proof of the Odd Order Theorem
- Learning-assisted theorem proving with millions of lemmas
- Mathematical Knowledge Management
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
- Aligning concepts across proof assistant libraries
- Deep Network Guided Proof Search
- Hammering towards QED
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- On well-ordered subsets of any set
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
- Intelligent computer mathematics. 9th international conference, CICM 2016, Bialystok, Poland, July 25--29, 2016. Proceedings
- Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings
- Accessing the Mizar Library with a Weakly Strict Mizar Parser
- Enhancement of Mizar Texts with Transitivity Property of Predicates
- System Description: E.T. 0.1
- Lattice Theory for Rough Sets – A Case Study with Mizar
- The 8th IJCAR automated theorem proving system competition – CASC-J8
- Large Formal Wikis: Issues and Solutions
- Mathematical Knowledge Management
- Mizar Course in Logic and Set Theory
- Automated Improving of Proof Legibility in the Mizar System
Cited In (only showing first 100 items - show all)
- An integrated web platform for the Mizar Mathematical Library
- Rings of fractions and localization
- About graph unions and intersections
- Formalization of quasilattices
- Grothendieck universes
- Partial correctness of a Fibonacci algorithm
- Renamings and a condition-free formalization of Kronecker's construction
- Unification of graphs and relations in Mizar
- Algebraic extensions
- Underlying simple graphs
- Algorithm NextFit for the bin packing problem
- On primary ideals. I
- Pappus's hexagon theorem in real projective plane
- Real vector space and related notions
- Some properties of membership functions composed of triangle functions and piecewise linear functions
- 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
- On roots of polynomials over \(F[X]/
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- Splitting fields
- Concatenation of finite sequences
- Automated Improving of Proof Legibility in the Mizar System
- A new export of the Mizar mathematical library
- Field extensions and Kronecker's construction
- Functional space consisted by continuous functions on topological space
- Some remarks about product spaces
- Finite dimensional real normed spaces are proper metric spaces
- Fundamental properties of fuzzy implications
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- On monomorphisms and subfields
- Continuity of bounded linear operators on normed linear spaces
- Zariski topology
- About regular graphs
- Mathematical Knowledge Management
- Human-centered automated proof search
- Ascoli-Arzelà theorem
- On weakly associative lattices and near lattices
- Quadratic extensions
- Reconstruction of the one-dimensional Lebesgue measure
- The 3-fold product space of real normed spaces and its properties
- Automatization of ternary Boolean algebras
- Duality notions in real projective plane
- Improper integral. I
- Improper integral. II
- Prime representing polynomial
- Relationship between the Riemann and Lebesgue integrals
- Invertible operators on Banach spaces
- Binary representation of natural numbers
- From LCF to Isabelle/HOL
- Diophantine sets. II
- Formalization of the MRDP theorem in the Mizar system
- Miscellaneous graph preliminaries
- Semantics of Mizar as an Isabelle object logic
- Mathematical knowledge management in MIZAR
- About graph mappings
- About vertex mappings
- AIM loops and the AIM conjecture
- On the intersection of fields \(F\) with \(F[X]\)
- Operations of points on elliptic curve in affine coordinates
- About supergraphs. I
- About supergraphs. II
- About graph sums
- On an algorithmic algebra over simple-named complex-valued nominative data
- Fubini's theorem
- Bilinear operators on normed linear spaces
- Embedding principle for rings and abelian groups
- Elementary number theory problems. IX
- Elementary number theory problems. X: Diophantine equations
- Elementary number theory problems. XI
- On fuzzy negations and laws of contraposition. Lattice of fuzzy negations
- Existence and uniqueness of algebraic closures
- Formalization of orthogonal decomposition for Hilbert spaces
- Prime representing polynomial with 10 unknowns -- introduction. II
- Prime representing polynomial with 10 unknowns
- Tarski geometry axioms. V: Half-planes and planes
- Ring and field adjunctions, algebraic elements and minimal polynomials
- Elementary number theory problems. VII
- Elementary number theory problems. VIII
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Implicit function theorem. II
- Isomorphisms from the space of multilinear operators
- Combining higher-order logic with set theory formalizations
- On bag of 1. I
- A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods
- Extended natural numbers and counters
- Functional sequence in norm space
- General theory and tools for proving algorithms in nominative data systems
- Partial correctness of an algorithm computing Lucas sequences
- Designing mathematical libraries based on minimal requirements for theorems
- Measure construction by extension in dependent type theory with application to integration
- Declarative Proof Translation (Short Paper)
- Introduction to algebraic geometry
- Elementary number theory problems. I
- Stability of the 7-3 compressor circuit for Wallace tree. I
- Elementary number theory problems. II
- Isosceles triangular and isosceles trapezoidal membership functions using centroid method
- On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors
Uses Software
This page was built for publication: The role of the Mizar mathematical library for interactive proof development in Mizar
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663215)
