Archive for the ‘Research’ Category

Proof Systems

Monday, January 18th, 2010

proof assistant author

  1. HOL John Harrison, Konrad Slind, Rob Arthan
  2. Mizar Andrzej Trybulec
  3. PVS Bart Jacobs, John Rushby
  4. Coq Laurent Thery, Pierre Letouzey, Georges Gonthier
  5. Otter/Ivy Michael Beeson, William McCune
  6. Isabelle/Isar Markus Wenzel, Larry Paulson
  7. Alfa/Agda Thierry Coquand
  8. ACL2 Ruben Gamboa
  9. PhoX Christophe Raffalli, Paul Roziµere
  10. IMPS William Farmer
  11. Metamath Norman Megill
  12. Theorema Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
  13. Lego Conor McBride
  14. Nuprl Paul Jackson
  15. mega Christoph BenzmÄuller, Armin Fiedler, Andreas Meier, Martin Pollet, JÄorg Siekmann
  16. B method Dominique Cansell
  17. Minlog Helmut Schwichtenberg

Tags:
Posted in Mathematics, Research | No Comments »

Mizar Math Library

Sunday, January 17th, 2010

Found this and consider as a right direction for formalizing mathematics knowledges. Going to spend time and promote  it among the Institute of Mathematics scientists.

Tags: ,
Posted in Research | No Comments »