Mizar: State-of-the-art and Beyond
From MaRDI portal
Publication:3453119
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
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 ⋮ Intuitionistic propositional calculus in the extended framework with modal operator. II ⋮ Compactness of neural networks ⋮ Splitting fields for the rational polynomials \(X^2 -2\), \(X^2+X+1\), \(X^3 -1\), and \(X^3 -2\) ⋮ Absolutely integrable functions ⋮ Non-trivial universes and sequences of universes ⋮ Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces ⋮ Characteristic subgroups ⋮ Transformation tools for real linear spaces ⋮ Definition of centroid method as defuzzification ⋮ Elementary number theory problems. III ⋮ On implicit and inverse function theorems on Euclidean spaces ⋮ Prime representing polynomial with 10 unknowns -- introduction ⋮ Artin's theorem towards the existence of algebraic closures ⋮ The divergence of the sum of prime reciprocals ⋮ Ring of endomorphisms and modules over a ring ⋮ Elementary number theory problems. IV ⋮ Elementary number theory problems. V ⋮ Elementary number theory problems. VI ⋮ Hammering Floating-Point Arithmetic ⋮ Learning Proof Transformations and Its Applications in Interactive Theorem Proving ⋮ Pell's equation ⋮ Embedding principle for rings and abelian groups ⋮ Elementary number theory problems. IX ⋮ Elementary number theory problems. X: Diophantine equations ⋮ Multidimensional measure space and integration ⋮ Elementary number theory problems. XI ⋮ Integral of continuous functions of two variables ⋮ Tarski geometry axioms. V: Half-planes and planes ⋮ Prime representing polynomial with 10 unknowns -- introduction. II ⋮ Prime representing polynomial with 10 unknowns ⋮ Existence and uniqueness of algebraic closures ⋮ Formalization of orthogonal decomposition for Hilbert spaces ⋮ A case study of transporting Urysohn's lemma from topology via open sets into topology via neighborhoods ⋮ Extended natural numbers and counters ⋮ Ring and field adjunctions, algebraic elements and minimal polynomials ⋮ Functional sequence in norm space ⋮ Elementary number theory problems. XIII ⋮ Integral of continuous three variable functions ⋮ Separable polynomials and separable extensions ⋮ Solving hard Mizar problems with instantiation and strategy invention ⋮ Remote verification system for Mizar integrated with emwiki ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MizAR 40 for Mizar 40
- MPTP-motivation, implementation, first experiments
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- An example of formalizing recent mathematical results in MIZAR
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- A compendium of continuous lattices in MIZAR
- A comparison of Mizar and Isar
- Eliciting implicit assumptions of Mizar proofs by property omission
- Methods of lemma extraction in natural deduction proofs
- ATP and presentation service for Mizar formalizations
- The Mizar Mathematical Library in OMDoc: translation and applications
- On rewriting rules in Mizar
- Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
- New Developments in Parsing Mizar
- Improving legibility of natural deduction proofs is not trivial
- MaLeCoP Machine Learning Connection Prover
- A Brief Overview of Mizar
- A Declarative Language for the Coq Proof Assistant
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- Large Formal Wikis: Issues and Solutions
- Licensing the Mizar Mathematical Library
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- A Symbolic Companion for Interactive Geometric Systems
- Efficient Rough Set Theory Merging
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- SAT-Enhanced Mizar Proof Checking
- Types for Proofs and Programs
- 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
- Mathematical Knowledge Management
This page was built for publication: Mizar: State-of-the-art and Beyond
