Mizar

swMATH4704MaRDI QIDQ16873FDOQ16873

Author name not available (Why is that?)

Described by source

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

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

• The future of logic: foundation-independence
• MMTTeX: connecting content and narration-oriented document formats
• User interaction with the Matita proof assistant
• Interpreting mathematical texts in Naproche-SAD
• Maintaining a library of formal mathematics
• A scalable module system
• Title not available (Why is that?)
• Event-based proof of the mutual exclusion property of Peterson's algorithm
• Propositional linear temporal logic with initial validity semantics
• Summable family in a commutative group
• Topology from neighbourhoods
• Stone lattices.
• Torsion part of \(\mathbb{Z}\)-module
• Mechanizing complemented lattices within Mizar type system
• Efficient Rough Set Theory Merging
• Collaborative Interactive Theorem Proving with Clide
• Representing model theory in a type-theoretical logical framework
• AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
• Object-free definition of categories
• On square-free numbers
• Prime filters and ideals in distributive lattices
• Groups -- additive notation.
• Two axiomatizations of Nelson algebras.
• The orthogonal projection and the Riesz representation theorem
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Automatic Proof and Disproof in Isabelle/HOL
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tools for MML Environment Analysis
• The Isabelle Framework
• The Lean Theorem Prover (System Description)
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Four decades of {\textsc{Mizar}}. Foreword
• Evidence algorithm and inference search in first-order logics
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Mining the Archive of Formal Proofs
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• The Mizar Mathematical Library in OMDoc: translation and applications
• TacticToe: Learning to Reason with HOL4 Tactics
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Matita Interactive Theorem Prover
• Implementation of the composition-nominative approach to program formalization in Mizar
• Flexary connectives in Mizar
• Automated reasoning and presentation support for formalizing mathematics in MizAR
• Parsing and Disambiguation of Symbolic Mathematics in the Naproche System
• A compendium of continuous lattices in MIZAR
• A comparison of Mizar and Isar
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• ATP and presentation service for Mizar formalizations
• Custom automations in Mizar
• Methods of lemma extraction in natural deduction proofs
• On rewriting rules in Mizar
• MPTP-motivation, implementation, first experiments
• On equivalents of well-foundedness. An experiment in MIZAR
• HOL(y)Hammer: online ATP service for HOL Light
• Categorical pullbacks
• The Isabelle/Naproche natural language proof assistant
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Formalising foundations of mathematics
• MPTP 0.2: Design, implementation, and initial experiments
• SAD as a mathematical assistant -- how should we go from here to there?
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• Formalization of real analysis: a survey of proof assistants and libraries
• Generic Literals
• Development of the theory of continuous lattices in MIZAR
• Mathematical knowledge management in MIZAR
• Automated Reasoning Service for HOL Light
• Using and parsing the Mizar language
• Automated and Human Proofs in General Mathematics: An Initial Comparison
• Challenges and Experiences in Managing Large-Scale Proofs
• Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar
• New Developments in Parsing Mizar
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• Tentative Experiments with Ellipsis in Mizar
• Improving legibility of natural deduction proofs is not trivial
• More SPASS with Isabelle
• Point-Free, Set-Free Concrete Linear Algebra
• Hammer for Coq: automation for dependent type theory
• ProofWatch: watchlist guidance for large theories in E
• ATPboost: learning premise selection in binary setting with ATP feedback
• Introduction to stopping time in stochastic finance theory. II
• Coquelicot: a user-friendly library of real analysis for Coq
• A Declarative Language for the Coq Proof Assistant
• Towards Self-verification of HOL Light
• 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
• Formalizing Physics: Automation, Presentation and Foundation Issues
• A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

This page was built for software: Mizar