Pages that link to "Item:Q1945905"
From MaRDI portal
The following pages link to ATP and presentation service for Mizar formalizations (Q1945905):
Displaying 30 items.
- Four decades of {\textsc{Mizar}}. Foreword (Q286794) (← links)
- Mechanizing complemented lattices within Mizar type system (Q286797) (← links)
- MizAR 40 for Mizar 40 (Q286800) (← links)
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver (Q286803) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- Flexary connectives in Mizar (Q1749141) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (Q2031406) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Formalization of quasilattices (Q2113839) (← links)
- Pappus's hexagon theorem in real projective plane (Q2119545) (← links)
- On weakly associative lattices and near lattices (Q2119547) (← links)
- On two alternative axiomatizations of lattices by McKenzie and Sholander (Q2311528) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Premise selection for mathematics by corpus analysis and kernel methods (Q2352489) (← links)
- Proof mining with dependent types (Q2364689) (← links)
- Pascal's theorem in real projective plane (Q2407506) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- Mizar: State-of-the-art and Beyond (Q3453119) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) (Q5049030) (← links)
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description (Q5495943) (← links)
- SAT-Enhanced Mizar Proof Checking (Q5495946) (← links)
- Superposition with lambdas (Q5918381) (← links)
- Superposition with lambdas (Q5919500) (← links)
