The role of the Mizar mathematical library for interactive proof development in Mizar

DOI10.1007/s10817-017-9440-6zbMath1433.68530OpenAlexW2770430340WikidataQ59610101 ScholiaQ59610101MaRDI QIDQ1663215

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

zbMATH Keywords

proof assistant Mizar mathematical library repository

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Mathematical knowledge management (68V30)

Related Items

Pappus's hexagon theorem in real projective plane ⋮ On weakly associative lattices and near lattices ⋮ Ascoli-Arzelà theorem ⋮ On primary ideals. I ⋮ Some properties of membership functions composed of triangle functions and piecewise linear functions ⋮ Real vector space and related notions ⋮ Splitting fields ⋮ Algorithm NextFit for the bin packing problem ⋮ A new export of the Mizar mathematical library ⋮ Miscellaneous graph preliminaries ⋮ Stability of the 7-3 compressor circuit for Wallace tree. I ⋮ Rings of fractions and localization ⋮ Reconstruction of the one-dimensional Lebesgue measure ⋮ Elementary number theory problems. I ⋮ Automatization of ternary Boolean algebras ⋮ Duality notions in real projective plane ⋮ Finite dimensional real normed spaces are proper metric spaces ⋮ Relationship between the Riemann and Lebesgue integrals ⋮ Improper integral. I ⋮ Prime representing polynomial ⋮ Quadratic extensions ⋮ The 3-fold product space of real normed spaces and its properties ⋮ About graph sums ⋮ Improper integral. II ⋮ Derivation of commutative rings and the Leibniz formula for power of derivation ⋮ Inverse function theorem. I ⋮ Miscellaneous graph preliminaries. I ⋮ Algebraic extensions ⋮ Functional space consisted by continuous functions on topological space ⋮ Elementary number theory problems. II ⋮ Concatenation of finite sequences ⋮ Bilinear operators on normed linear spaces ⋮ 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 ⋮ Tarski geometry axioms. IV: Right angle ⋮ Maximum number of steps taken by modular exponentiation and Euclidean algorithm ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ On bag of 1. I ⋮ Differentiation on interval ⋮ Elementary number theory problems. VII ⋮ Introduction to graph enumerations ⋮ On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors ⋮ Isosceles triangular and isosceles trapezoidal membership functions using centroid method ⋮ Introduction to algebraic geometry ⋮ About regular graphs ⋮ Elementary number theory problems. VIII ⋮ Extending numeric automation for number theory formalizations in Mizar ⋮ An integrated web platform for the Mizar Mathematical Library ⋮ Combining higher-order logic with set theory formalizations ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Declarative Proof Translation (Short Paper) ⋮ Automated Comparative Study of Some Generalized Rough Approximations ⋮ From LCF to Isabelle/HOL ⋮ On the intersection of fields \(F\) with \(F[X\)] ⋮ Field extensions and Kronecker's construction ⋮ Underlying simple graphs ⋮ About graph mappings ⋮ About vertex mappings ⋮ Operations of points on elliptic curve in affine coordinates ⋮ AIM loops and the AIM conjecture ⋮ Parity as a property of integers ⋮ About supergraphs. I ⋮ About supergraphs. II ⋮ 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 ⋮ Basic Diophantine relations ⋮ On two alternative axiomatizations of lattices by McKenzie and Sholander ⋮ Arithmetic operations on short finite sequences ⋮ Some remarks about product spaces ⋮ Binary representation of natural numbers ⋮ Continuity of bounded linear operators on normed linear spaces ⋮ Pythagorean tuning: pentatonic and heptatonic scale ⋮ Fundamental properties of fuzzy implications ⋮ Zariski topology ⋮ Human-centered automated proof search ⋮ Semantics of Mizar as an Isabelle object logic ⋮ On roots of polynomials over \(F[X/

\)] ⋮ Isomorphisms from the space of multilinear operators ⋮ Invertible operators on Banach spaces ⋮ Implicit function theorem. II ⋮ On monomorphisms and subfields ⋮ Partial correctness of a factorial algorithm ⋮ Partial correctness of a power algorithm ⋮ Diophantine sets. II ⋮ Formalization of the MRDP theorem in the Mizar system ⋮ Renamings and a condition-free formalization of Kronecker's construction ⋮ About graph unions and intersections ⋮ Unification of graphs and relations in Mizar ⋮ Partial correctness of a Fibonacci algorithm ⋮ Grothendieck universes ⋮ Formalization of quasilattices

Uses Software

Cites Work