Four decades of {\textsc{Mizar}}. Foreword

DOI10.1007/s10817-015-9345-1zbMath1336.00111OpenAlexW2184838578WikidataQ59407702 ScholiaQ59407702MaRDI QIDQ286794

No author found.

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

zbMATH Keywords

natural deduction computer proof assistant formalization of mathematics Mizar Mizar mathematical library

Mathematics Subject Classification ID

Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to computer science (68-06) Mechanization of proofs and logical operations (03B35) Applications of set theory (03E75) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06)

Related Items

Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ Eliminating models during model elimination ⋮ Aligning concepts across proof assistant libraries ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ About graph complements ⋮ Stability of the 7-3 compressor circuit for Wallace tree. I ⋮ About graph sums ⋮ 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 ⋮ Differentiation on interval ⋮ Introduction to graph enumerations ⋮ Introduction to algebraic geometry ⋮ About regular graphs ⋮ Elementary number theory problems. VIII ⋮ 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 ⋮ 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 ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Declarative Proof Translation (Short Paper) ⋮ Binary relations-based rough sets -- an automated approach ⋮ Tarski geometry axioms. II ⋮ Automated Comparative Study of Some Generalized Rough Approximations ⋮ From LCF to Isabelle/HOL ⋮ 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 ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates ⋮ 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 ⋮ What’s in a Theorem Name? ⋮ 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 ⋮ 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 ⋮ 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

Uses Software

Cites Work