Mizar: State-of-the-art and Beyond

DOI10.1007/978-3-319-20615-8_17zbMath1417.68201OpenAlexW2295728669MaRDI QIDQ3453119

Artur Korniłowicz, Adam Naumowicz, Roman Matuszewski, Josef Urban, Adam Grabowski, Karol Pąk, Czesław Byliński, Grzegorz Bancerek

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-20615-8_17

Mathematics Subject Classification ID

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (only showing first 100 items - show all)

Computer Certification of Generalized Rough Sets Based on Relations ⋮ Reconstruction of the one-dimensional Lebesgue measure ⋮ Elementary number theory problems. I ⋮ On fuzzy negations generated by fuzzy implications ⋮ Derivation of commutative rings and the Leibniz formula for power of derivation ⋮ Inverse function theorem. I ⋮ Algebraic extensions ⋮ Functional space consisted by continuous functions on topological space ⋮ Elementary number theory problems. II ⋮ On bag of 1. I ⋮ Differentiation on interval ⋮ Elementary number theory problems. VII ⋮ On the formalization of Gram-Schmidt process for orthonormalizing a set of vectors ⋮ Isosceles triangular and isosceles trapezoidal membership functions using centroid method ⋮ Internal direct products and the universal property of direct product groups ⋮ : A Linear Algebra Textbook System ⋮ Pell's equation ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates ⋮ 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 ⋮ Algorithm NextFit for the bin packing problem ⋮ Summable family in a commutative group ⋮ Topology from neighbourhoods ⋮ Torsion part of \(\mathbb{Z}\)-module ⋮ Event-based proof of the mutual exclusion property of Peterson's algorithm ⋮ Propositional linear temporal logic with initial validity semantics ⋮ Stone lattices. ⋮ Deepalgebra -- an outline of a program ⋮ Semantic representation of general topology in the Wolfram language ⋮ Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema ⋮ Generating custom set theories with non-set structured objects ⋮ Modelling real world using stochastic processes and filtration ⋮ Circumcenter, circumcircle and centroid of a triangle ⋮ Altitude, orthocenter of a triangle and triangulation ⋮ Divisible \(\mathbb{Z}\)-modules ⋮ Lattice of \(\mathbb{Z}\)-module ⋮ Product pre-measure ⋮ Conservation rules of direct sum decomposition of groups ⋮ Aligning concepts across proof assistant libraries ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Hammer for Coq: automation for dependent type theory ⋮ Klein-Beltrami model. III ⋮ Klein-Beltrami model. IV ⋮ Miscellaneous graph preliminaries ⋮ Stability of the 7-3 compressor circuit for Wallace tree. I ⋮ Rings of fractions and localization ⋮ 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 ⋮ Improper integral. II ⋮ Vieta's formula about the sum of roots of polynomials ⋮ Basic formal properties of triangular norms and conorms ⋮ Pascal's theorem in real projective plane ⋮ About quotient orders and ordering sequences ⋮ Basel problem -- preliminaries ⋮ Basel problem ⋮ Dual lattice of \(\mathbb{Z}\)-module lattice ⋮ Cross-ratio in real vector space ⋮ Continuity of multilinear operator on normed linear spaces ⋮ Tarski geometry axioms. IV: Right angle ⋮ Maximum number of steps taken by modular exponentiation and Euclidean algorithm ⋮ Isomorphism theorem on vector spaces over a ring ⋮ F. Riesz theorem ⋮ On roots of polynomials and algebraically closed fields ⋮ Gauge integral ⋮ Integral of non positive functions ⋮ From types to sets by local type definition in higher-order logic ⋮ Compactness in metric spaces ⋮ Double sequences and iterated limits in regular space ⋮ Prime factorization of sums and differences of two like powers ⋮ Riemann-Stieltjes integral ⋮ Quasi-uniform space ⋮ Uniform space ⋮ Some algebraic properties of polynomial rings ⋮ Homography in \(\mathbb{R}\mathbb{P}^2\) ⋮ A generic and executable formalization of signature-based Gröbner basis algorithms ⋮ 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 ⋮ Sequences of prime reciprocals. Preliminaries ⋮ On the intersection of fields \(F\) with \(F[X\)] ⋮ Operations of points on elliptic curve in affine coordinates ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Mizar

Uses Software

Cites Work

This page was built for publication: Mizar: State-of-the-art and Beyond