The following pages link to Mizar (Q16873):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Summable family in a commutative group (Q271890) (← links)
- Topology from neighbourhoods (Q271891) (← links)
- Torsion part of \(\mathbb{Z}\)-module (Q271895) (← links)
- Event-based proof of the mutual exclusion property of Peterson's algorithm (Q271900) (← links)
- Propositional linear temporal logic with initial validity semantics (Q271908) (← links)
- Stone lattices. (Q271910) (← links)
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Mechanizing complemented lattices within Mizar type system (Q286797) (← links)
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization (Q286801) (← links)
- Evidence algorithm and inference search in first-order logics (Q286802) (← links)
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver (Q286803) (← links)
- Improving legibility of formal proofs based on the close reference principle is NP-hard (Q286805) (← links)
- Modelling real world using stochastic processes and filtration (Q306626) (← links)
- Circumcenter, circumcircle and centroid of a triangle (Q306627) (← links)
- Altitude, orthocenter of a triangle and triangulation (Q306628) (← links)
- Divisible \(\mathbb{Z}\)-modules (Q306629) (← links)
- Lattice of \(\mathbb{Z}\)-module (Q306630) (← links)
- Product pre-measure (Q306631) (← links)
- Conservation rules of direct sum decomposition of groups (Q306634) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006 (Q373628) (← links)
- A scalable module system (Q391632) (← links)
- Polygonal numbers (Q467780) (← links)
- On square-free numbers (Q467787) (← links)
- Formalization of the Advanced Encryption Standard. I (Q467789) (← links)
- Object-free definition of categories (Q467791) (← links)
- Prime filters and ideals in distributive lattices (Q467793) (← links)
- Introduction to formal preference spaces (Q467795) (← links)
- Formulation of cell Petri nets (Q467800) (← links)
- Definition of flat poset and existence theorems for recursive call (Q467805) (← links)
- Topological interpretation of rough sets (Q467816) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- Two axiomatizations of Nelson algebras. (Q491776) (← links)
- Groups -- additive notation. (Q491777) (← links)
- Fermat's little theorem via divisibility of Newton's binomial (Q500025) (← links)
- Weak convergence and weak\(^\ast\) convergence (Q500026) (← links)
- The orthogonal projection and the Riesz representation theorem (Q500027) (← links)
- Binary relations-based rough sets -- an automated approach (Q502682) (← links)
- Tarski geometry axioms. II (Q502683) (← links)
- Term context (Q502697) (← links)
- Cauchy mean theorem (Q502698) (← links)
- Tarski geometry axioms (Q502700) (← links)
- Topological manifolds (Q502702) (← links)
- Proof verification and proof discovery for relativity (Q514557) (← links)
- Compactness in metric spaces (Q516741) (← links)
- Double sequences and iterated limits in regular space (Q516742) (← links)
