The following pages link to (Q3075247):
Displaying 50 items.
- Mizar (Q16873) (← links)
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Mechanizing complemented lattices within Mizar type system (Q286797) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization (Q286801) (← 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)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
- A consistent foundation for Isabelle/HOL (Q1739913) (← links)
- Flexary connectives in Mizar (Q1749141) (← links)
- Eliciting implicit assumptions of Mizar proofs by property omission (Q1945901) (← links)
- Methods of lemma extraction in natural deduction proofs (Q1945902) (← links)
- ATP and presentation service for Mizar formalizations (Q1945905) (← links)
- The Mizar Mathematical Library in OMDoc: translation and applications (Q1945907) (← links)
- On rewriting rules in Mizar (Q1945908) (← links)
- Custom automations in Mizar (Q1945910) (← links)
- Improving stateful premise selection with transformers (Q2128800) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- Initial Comparison of Formal Approaches to Fuzzy and Rough Sets (Q2814146) (← links)
- Accessing the Mizar Library with a Weakly Strict Mizar Parser (Q2817295) (← links)
- Extracting Higher-Order Goals from the Mizar Mathematical Library (Q2817297) (← links)
- Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems (Q2817922) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- New Developments in Parsing Mizar (Q2907343) (← links)
- Checking Proofs (Q2950035) (← links)
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math” (Q3100213) (← links)
- Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets (Q3300368) (← links)
- Readable Formalization of Euler’s Partition Theorem in Mizar (Q3453116) (← links)
- Mizar: State-of-the-art and Beyond (Q3453119) (← links)
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library (Q3453131) (← links)
- Tools for MML Environment Analysis (Q3453132) (← links)
- The Proof Certifier Checkers (Q3455771) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 (Q5145435) (← links)
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library (Q5200124) (← links)
- Automated Improving of Proof Legibility in the Mizar System (Q5495936) (← links)
- SAT-Enhanced Mizar Proof Checking (Q5495946) (← links)
- Hammering Mizar by Learning Clause Guidance (Short Paper). (Q5875448) (← links)
- Formalization of the fundamental group in untyped set theory using auto2 (Q5915787) (← links)
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} (Q5919026) (← links)
- Conway numbers -- formal introduction (Q6557120) (← links)
