Fetching the paper…
Reading the bibliography…
This paper describes the Automated Reasoning for Mizar (MizAR) service, which integrates several automated reasoning, artificial intelligence, and presentation tools with Mizar and its authoring environment.
Sur le coloriage des graphes
Jan Mycielski · 1955
Earlier work this paper cites.
The Ordinal Numbers
G. Bancerek · 1990
Earlier work this paper cites.
Optimizing Proof Search in Model Elimination
J. Harrison · 1996
Earlier work this paper cites.
First-order Proof Problems Extracted from an Article in the MIZAR Mathematical Library
Ingo Dahn and Christoph Wernhard · 1997
Earlier work this paper cites.
SystemOnTPTP
G. Sutcliffe · 2000
Earlier work this paper cites.
First-order proof tactics in higher-order logic theorem provers
Joe Hurd · 2003
Earlier work this paper cites.
A Proof of the Kepler Conjecture
T. Hales · 2005
Earlier work this paper cites.
XML-izing Mizar: Making Semantic Processing and Presentaion of MML Easy
J. Urban · 2005
Earlier work this paper cites.
MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics
J. Urban · 2006
Earlier work this paper cites.
MPTP 0.2: Design, implementation, and initial experiments
Josef Urban · 2006
Cited alongside, same era.
First Order Reasoning on a Large Ontology
A. Pease and G. Sutcliffe · 2007
Cited alongside, same era.
A Special Issue on Formal Proof of Notices of the AMS
T. Hales, editor · 2008
Cited alongside, same era.
ATP-based cross-verification of Mizar proofs: Method, systems, and first experiments
Josef Urban and Geoff Sutcliffe · 2008
Cited alongside, same era.
MaLARea SG1- machine learner for automated reasoning with semantic guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil · 2008
Cited alongside, same era.
seL4: Formal Verification of an OS Kernel
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood · 2009
Cited alongside, same era.
Three Years of Experience with Sledgehammer, a Practical Link between Automated and Interactive Theorem Provers
Lawrence C. Paulson and Jasmin C. Blanchette · 2010
Later among the works it cites.
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
Josef Urban, Jesse Alama, Piotr Rudnicki, and Herman Geuvers · 2010
Later among the works it cites.
Evaluation of automated theorem proving on the Mizar mathematical library
Josef Urban, Kryštof Hoder, and Andrei Voronkov · 2010
Later among the works it cites.
Automated proof compression by invention of new definitions
Jirí Vyskocil, David Stanovský, and Josef Urban · 2010
Later among the works it cites.
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
J. Alama, D. Kühlwein, E. Tsivtsivadze, J. Urban, and T. Heskes · 2011
Closest in time.
Sine Qua Non for Large Theory Reasoning
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Lightweight Relevance Filtering for Machine-generated Resolution Problems
Jia Meng and Lawrence C. Paulson · 2009
Cited alongside, same era.
Mizar in a Nutshell
Grabowski A., Kornilowicz A., and Naumowicz A · 2010
Cited alongside, same era.
K. Hoder and A. Voronkov · 2011
Closest in time.
Simple graphs as simplicial complexes: the Mycielskian of a graph
Piotr Rudnicki and Lorna Stewart · 2012
Closest in time.
Josef Urban · 2012
Closest in time.