Mizar

swMATH4704MaRDI QIDQ16873FDOQ16873

Author name not available (Why is that?)

Described by source

• MizAR 40 for Mizar 40
• A Brief Overview of Mizar
• Mizar: state-of-the-art and beyond
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• The seventeen provers of the world. Foreword by Dana S. Scott..
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8--13, 2012. Proceedings
• On duplication in mathematical repositories
• Isabelle formalization of set theoretic structures and set comprehensions
• JEFL: joint embedding of formal proof libraries
• Vampire with a brain is a good ITP hammer
• Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
• Tarski geometry axioms. III
• Title not available (Why is that?)
• How to write a 21\(^{\text{st}}\) century proof
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• Title not available (Why is that?)
• Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
• Aligning concepts across proof assistant libraries
• Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3--6, 2001. Proceedings
• Mechanizing Mathematical Reasoning
• About graph complements
• Proceedings of the workshop on mathematics, logic and computation (satellite event of ICALP 2003), Valencia, Spain, June 12--14, 2003
• Field extensions and Kronecker's construction
• Deep network guided proof search
• A proof-centric approach to mathematical assistants
• Supporting the formal verification of mathematical texts
• Conway's games and some of their basic properties
• Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
• Computer theorem proving in mathematics
• Applying, extending, and specializing pseudorecursiveness
• ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
• Mizar’s Soft Type System
• Classification of alignments between concepts of formal mathematical systems
• Monte Carlo tableau proof search
• Transition of consistency and satisfiability under language extensions
• Implementing geometric algebra products with binary trees
• Reconstruction of the one-dimensional Lebesgue measure
• A machine-checked implementation of Buchberger's algorithm
• On roots of polynomials and algebraically closed fields
• A refinement of de Bruijn's formal language of mathematics
• Symbolic computation and automated reasoning. The CALCULEMUS-2000 symposium. 8th symposium on the integration of symbolic computation and mechanized reasoning, St. Andrews, Scotland, GB, August 6--7, 2000
• Formalization of generalized almost distributive lattices.
• Fermat's little theorem via divisibility of Newton's binomial
• Weak convergence and weak\(^\ast\) convergence
• Binary relations-based rough sets -- an automated approach
• Cauchy mean theorem
• Tarski geometry axioms. II
• Term context
• Topological manifolds
• Representing model theory in a type-theoretical logical framework
• Automated theorem provers: a practical tool for the working mathematician?
• Title not available (Why is that?)
• Defining power series and polynomials in Mizar
• Type theory and formal proof. An introduction
• Proof verification and proof discovery for relativity
• Compactness in metric spaces
• Double sequences and iterated limits in regular space
• Prime factorization of sums and differences of two like powers
• Quasi-uniform space
• Riemann-Stieltjes integral
• Some algebraic properties of polynomial rings
• Uniform space
• Homography in \(\mathbb{R}\mathbb{P}^2\)
• Hammering towards QED
• A logical framework combining model and proof theory
• Introduction to Diophantine approximation. II
• Analysis of algorithms: an example of a sort algorithm
• Relational formal characterization of rough sets
• Veblen hierarchy
• Automated search for impossibility theorems in social choice theory: ranking sets of objects
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
• Lemma Mining over HOL Light
• Title not available (Why is that?)
• Title not available (Why is that?)
• Robbins algebras vs. Boolean algebras
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• First order languages: further syntax and semantics
• Preliminaries to classical first-order model theory
• Towards MKM in the large: modular representation and scalable software architecture
• Automated Discovery of Properties of Rough Sets
• Revisions as an Essential Tool to Maintain Mathematical Repositories
• Towards logical frameworks in the heterogeneous tool set Hets
• Extending MKM formats at the statement level
• A query language for formal mathematical libraries
• Commutative algebra in the Mizar system
• Information Retrieval and Rendering with MML Query
• Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15--19, 2007. Proceedings
• Altitude, orthocenter of a triangle and triangulation
• Circumcenter, circumcircle and centroid of a triangle
• Conservation rules of direct sum decomposition of groups
• Divisible \(\mathbb{Z}\)-modules
• Lattice of \(\mathbb{Z}\)-module
• Modelling real world using stochastic processes and filtration
• Product pre-measure
• Mechanically proving termination using polynomial interpretations
• An example of formalizing recent mathematical results in MIZAR
• The Jordan Curve Theorem, Formally and Informally
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• Definition of flat poset and existence theorems for recursive call

This page was built for software: Mizar