- 1992-95: the QED dream. Bob Boyer, Rusty Lusk. Later Bill McCune, Larry Was, Bill McCarthy, Andrzej Trybulec, Piotr Rudnicki, Ingo Dahn, Tomas Jech, John Harrison, Claus Zinn, Andrzej Tarlecki, Randall Holmes, Paul Jackson, Deepak Kapur, Javier Thayer ... .
- 1994-98: the ILF system. Ingo Dahn, Christoph Wernhard, Czeslaw Bylinski.
- 2002: the MoMM system (Most of Mizar Matches)
- 2003: first version of the MPTP system (Mizar Problems for Theorem Proving)
- 2003: first version of the Mizar Proof Advisor
- 2005: second version of MPTP
- 2006: the MPTP Challenges - stimulation of the ATP for Mizar research
- 2007: first version of MaLARea (Machine Learner for Automated Reasoning)
- 2007: the SRASS system. Jiri Vyskocil, Petr Pudlak and Geoff Sutcliffe.
- 2008: the SInE axiom selection system. Krystof Hoder.
- 2008: the CASC-LTB competition.
- 2008: MaLARea with Semantic Guidance.
- 2010: the MizAR presentation, verification and ATP service.
Josef Urban
2011-01-14
