Found 12 Documents (Results 1–12)
The role of the Mizar mathematical library for interactive proof development in Mizar. (English) Zbl 1433.68530
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. (English) Zbl 1425.68381
MSC:
68T15
A learning-based fact selector for Isabelle/HOL. (English) Zbl 1386.68149
MSC:
68T15
68T05
MizAR 40 for Mizar 40. (English) Zbl 1356.68191
MSC:
68T15
68T05
Premise selection for mathematics by corpus analysis and kernel methods. (English) Zbl 1315.68217
MSC:
68T15
68T05
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). (English) Zbl 1314.68283
J. Autom. Reasoning 53, No. 2, 173-213 (2014); erratum ibid. 54, No. 1, 99 (2015).
MSC:
68T15
68T05
The Mizar Mathematical Library in OMDoc: translation and applications. (English) Zbl 1260.68375
MSC:
68T15
68T30
ATP and presentation service for Mizar formalizations. (English) Zbl 1260.68380
MSC:
68T15
Eliciting implicit assumptions of Mizar proofs by property omission. (English) Zbl 1260.68361
MSC:
68T15
The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0. (English) Zbl 1185.68636
MSC:
68T15
MPTP 0.2: Design, implementation, and initial experiments. (English) Zbl 1113.68095
MSC:
68T15
Filter Results by …
all
top 5
Author
- Urban, Josef (7)
- Kaliszyk, Cezary (4)
- Sutcliffe, Geoff (3)
- Alama, Jesse (2)
- Kühlwein, Daniel (2)
- Pąk, Karol (2)
- Bancerek, Grzegorz (1)
- Blanchette, Jasmin Christian (1)
- Byliński, Czesław (1)
- Grabowski, Adam (1)
- Greenaway, David (1)
- Heskes, Tom M. (1)
- Iancu, Mihnea (1)
- Kohlhase, Michael (1)
- Korniłowicz, Artur (1)
- Matuszewski, Roman (1)
- Naumowicz, Adam (1)
- Rabe, Florian (1)
- Rudnicki, Piotr (1)
- Tsivtsivadze, Evgeni (1)
all
top 5
Volume
- 63, No. 3 (2019) (1)
- 61, No. 1-4 (2018) (1)
- 59, No. 4 (2017) (1)
- 57, No. 3 (2016) (1)
- 55, No. 3 (2015) (1)
- 53, No. 2 (2014) (1)
- 52, No. 2 (2014) (1)
- 50, No. 2 (2013) (3)
- 43, No. 4 (2009) (1)
- 37, No. 1-2 (2006) (1)
all
top 3
Software
- MPTP 0.2 (12)
- Mizar (10)
- MaLARea (7)
- E Theorem Prover (6)
- MML (6)
- MPTP (6)
- MoMM (6)
- Isabelle/HOL (5)
- Sledgehammer (5)
- VAMPIRE (5)
- kepler98 (5)
- z3 (5)
- Flyspeck (4)
- HOL Light (4)
- Metis_ (4)
- OMDoc (4)
- BliStr (3)
- MizarMode (3)
- OTTER (3)
- SPASS (3)
- TPTP (3)
- Twelf (3)
- seL4 (3)
- ACL2 (2)
- Archive Formal Proofs (2)
- CSPLib (2)
- Coq (2)
- HOLyHammer (2)
- IDV (2)
- ILTP (2)
- Isar (2)
- Ivy (2)
- LEO-II (2)
- Logic2CNF (2)
- MaSh (2)
- SATLIB (2)
- SMT-LIB (2)
- SystemOnTPTP (2)
- miz3 (2)
- mizar-items (2)
- AVATAR (1)
- Automath (1)
- CVC4 (1)
- Caduceus (1)
- CeTA (1)
- DeepMath (1)
- FOOL (1)
- Gandalf (1)
- HOL (1)
- HOL Zero (1)
- I-SATCHMO (1)
- Isabelle (1)
- Isabelle/Isar (1)
- Isabelle/PIDE (1)
- Isabelle/ZF (1)
- Jinja not Java (1)
- KRAKATOA (1)
- LATIN (1)
- LPL software (1)
- Lean (1)
- ML (1)
- MMT (1)
- MaLeCoP (1)
- Mace4 (1)
- MathWebSearch (1)
- Metamath (1)
- MetiTarski (1)
- Nitpick (1)
- Nominal Isabelle (1)
- Octopus (1)
- PERL (1)
- PRMLT (1)
- PRocH (1)
- Pegasos (1)
- ProofPeer (1)
- Prover9 (1)
- QBFEVAL (1)
- Rodin (1)
- SAD (1)
- SATCHMO (1)
- SMTtoTPTP (1)
- SNARK (1)
- SPASS+T (1)
- SRASS (1)
- Satallax (1)
- SigmaKEE (1)
- THF0 (1)
- TNTBase (1)
- TPS (1)
- TRAMP (1)
- Tipi (1)
- Waldmeister (1)
- Why3 (1)
- YAGO (1)
- Zenon (1)
- gensim (1)
- ileanCoP (1)
- leanCoP (1)
- veriT (1)