Mizar
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Formalizing Arrow's theorem
- Proving properties of Pascal programs in MIZAR 2
- Erratum to: Proving properties of Pascal programs in MIZAR 2
- ALCOR
- ACL2
- Coq
- Isabelle
- LEO-II
- mizar-items
- Proviola
- lazyCoP
- Goeland
- Theorema
- TPS
- ML
- Mathematical knowledge management. Second international conference, MKM 2003, Bertinoro, Italy, February 16--18, 2003. Proceedings
- Vivid
- Isabelle/HOL
- MizarMode
- Isabelle/Isar
- IsaPlanner
- CASL
- MPTP
- MPTP 0.2
- TADD
- OTTER
- VAMPIRE
- THF0
- MAYA
- A machine-checked implementation of Buchberger's algorithm
- PVS
- CoqEAL
- MathWebSearch
- gensim
- SPASS
- TPTP
- Aligning concepts across proof assistant libraries
- Implementation of the composition-nominative approach to program formalization in Mizar
- Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings
- Metis
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Hammer for Coq: automation for dependent type theory
- Isar
- MoMM
- Making PVS accessible to generic services by interpretation in a universal format
- 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
- Formal introduction to fuzzy implications
- LPL software
- IsaWin
- TAS
- Proof General
- Prover9
- Isabelle/ZF
- From types to sets by local type definition in higher-order logic
- A consistent foundation for Isabelle/HOL
- Flexary connectives in Mizar
- TeXmacs
- HOL
- Kaprekar Series Generator
- ASCIIMathML
- ProofWatch: watchlist guidance for large theories in E
- Formally real fields
- Introduction to stopping time in stochastic finance theory. II
- Implicit function theorem. I
- Introduction to Diophantine approximation. II
- Tarski geometry axioms. III
- The Matiyasevich theorem. Preliminaries
- Introduction to stochastic finance: random variables and arbitrage theory
- Kleene algebra of partial predicates
- Klein-Beltrami model. I
- Klein-Beltrami model. II
- Fubini's theorem for non-negative or non-positive functions
- Sequences of prime reciprocals. Preliminaries
- Diophantine sets. Preliminaries
- System description: XSL-based translator of Mizar to {\LaTeX}
- Translating the IMPS theory library to MMT/OMDoc
- Isabelle import infrastructure for the Mizar Mathematical Library
- Gröbner bases of modules and Faugère's F₄ algorithm in Isabelle/HOL
- First experiments with neural translation of informal to formal mathematics
- ATPboost: learning premise selection in binary setting with ATP feedback
- Theories as types
- An overview of a formal framework for managing mathematics
- Designing mathematical libraries based on requirements for theorems
- Matita
- A set theory with support for partial functions
- ETPS
- ProofPower
- AEtnaNova
- ActiveMath
- PIDE
- Isabelle/jEdit
- HOL Light
- HOL-Omega
- A compendium of continuous lattices in MIZAR
This page was built for software: Mizar
