Digital Math by Logic

This is an overview of systems implementing "mathematics in the computer" as compiled by Freek Wiedijk. Similar information can be found at:

This is the version that is sorted by the logic that is supported. There also are versions with samples and in stylish text. And there also are versions of this list grouped by alphabet, by implementation language, by category, by most common interaction mode, and by the size of the effort. Finally, there is a short explanation of the various fields in this database.

This information is still incomplete and there probably are some errors in it. I would appreciate it if people would help me correct and complete it.

Both

1. Akka: Web Page: http://turing.wins.uva.nl/~lhendrik/AkkaStart.html
E-Mail: lhendrik@wins.uva.nl
Architect: Lex Hendriks
Language: Tcl
Category: Logic Education
Interaction: Unknown, Logic: Both, Size: Small

2. CYP: Web Page: ftp://ftp-sop.inria.fr/lemme/cyp/index.html
E-Mail: thery@sophia.inria.fr
Architect: Laurent Théry
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Both, Size: Small

3. Fellowship: Web Page: http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/fellowship/
E-Mail: Unknown
Architect: Florent Kirchner, Claudio Sacerdoti Coen
Language: Objective CAML
Category: Tactic Prover
Interaction: Dialog, Logic: Both, Size: Small

4. FLiP: Web Page: http://staff.washington.edu/jon/flip/www/
E-Mail: jon@washington.edu
Architect: Jonathan Jacky
Language: Python
Category: Proof Checker
Interaction: Dialog, Logic: Both, Size: Small

5. Gandalf: Web Page: http://www.cs.chalmers.se/~tammet/gandalf/
E-Mail: tammet@cs.chalmers.se
Architect: Tanel Tammet
Language: Scheme
Category: First Order Prover
Interaction: Script, Logic: Both, Size: Small

6. ICLE: Web Page: http://www.doc.ic.ac.uk/~md/
E-Mail: md@doc.ic.ac.uk
Architect: Mark Dawson
Language: Omega Prolog
Category: Proof Checker
Interaction: Editor, Logic: Both, Size: Small

7. Isabelle: Web Page: http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Mailing List: isabelle-users@cl.cam.ac.uk
Architect: Larry Paulson, e.a.
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Both, Size: Large

8. Isabelle: Isar: Web Page: http://isabelle.in.tum.de/Isar/
E-Mail: wenzelm@in.tum.de
Architect: Markus Wenzel
Language: Standard ML
Category: Tactic Prover
Interaction: Editor, Logic: Both, Size: Small

9. Jape: Web Page: http://users.comlab.ox.ac.uk/bernard.sufrin/jape.html
E-Mail: Unknown
Architect: Bernard Sufrin, Richard Bornat
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small

10. Logics Workbench, LWB: Web Page: http://www.lwb.unibe.ch/
E-Mail: lwb@iam.unibe.ch
Architect: Gerhard Jaeger
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small

11. MacLogic: Web Page: http://www-theory.dcs.st-and.ac.uk/~rd/logic/mac/
E-Mail: rd@dcs.st-and.ac.uk
Architect: Roy Dyckhoff
Language: MacProlog
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small

12. OBJ: Web Page: http://archive.comlab.ox.ac.uk/obj.html
E-Mail: Unknown
Architect: Joseph Goguen
Language: Common Lisp
Category: Specification Environment
Interaction: Interface, Logic: Both, Size: Large

13. Proof General: Web Page: http://proofgeneral.inf.ed.ac.uk/
E-Mail: proofgen@dcs.ed.ac.uk
Architect: Thomas Kleymann, e.a.
Language: Emacs Lisp
Category: Authoring
Interaction: Editor, Logic: Both, Size: Small

14. Theax: Web Page: http://markun.cs.shinshu-u.ac.jp/kiso/projects/mathematics/Theax-e/Math-e-tit.htm
E-Mail: ynakamur@cs.shinshu-u.ac.jp
Architect: Yatsuka Nakamura
Language: Pascal, C
Category: Proof Checker
Interaction: Batch, Logic: Both, Size: Small

15. TinkerType: Web Page: http://www.cis.upenn.edu/~bcpierce/papers/modular-bib.html#LevinPierce99
E-Mail: milevin@cis.upenn.edu
Architect: Michael Levin, Benjamin Pierce
Language: Objective CAML
Category: Proof Checker
Interaction: Script, Logic: Both, Size: Small

Classical

16. 3TaP: Web Page: http://mathforum.org/library/view/17325.html
E-Mail: beckert@uni-koblenz.de
Architect: Reiner Haehnle, Bernhard Beckert
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

17. ACL2: Web Page: http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html
E-Mail: Unknown
Architect: J. Strother Moore, e.a.
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

18. Alfie: Web Page: http://www.cs.chalmers.se/~sydow/alfie/index.html
E-Mail: Unknown
Architect: Björn von Sydow
Language: Haskell
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small

19. Analytica: Web Page: http://andrej.com/analytica/
E-Mail: Edmund.Clarke@cs.cmu.edu
Architect: Edmund Clarke, Xudong Zhao
Language: Mathematica
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

20. Automath: Aut: Web Page: http://www.cs.ru.nl/~freek/aut/
E-Mail: freek@cs.kun.nl
Architect: Freek Wiedijk
Language: C
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

21. Bertie3, Twootie: Web Page: http://www.ucc.uconn.edu/~wwwphil/software.html
E-Mail: aclark@uconnvm.uconn.edu
Architect: Austen Clark
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small

22. Bertrand: Web Page: http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html
E-Mail: herzberg@kagi.com
Architect: Larry Herzberg
Language: Unknown
Category: First Order Prover
Interaction: Editor, Logic: Classical, Size: Small

23. Bliksem: Web Page: http://www.mpi-sb.mpg.de/~nivelle/programs/bliksem/
E-Mail: nivelle@mpi-sb.mpg.de
Architect: Hans de Nivelle
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

24. Class: Web Page: http://class-int.narod.ru
E-Mail: urchick@mail.ru
Architect: Yuri Vtorushin, Oleg Okhotnikov
Language: C++
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

25. CLIN: Web Page: http://www.cs.unc.edu/Research/mi/mi-provers.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

26. Cocktail: Web Page: http://www.win.tue.nl/~michaelf/cocktail.html
E-Mail: michaelf@win.tue.nl
Architect: Michael Franssen
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

27. Coq: Pcoq: Web Page: http://www-sop.inria.fr/lemme/pcoq/
E-Mail: bertot@paprika.inria.fr
Architect: Yves Bertot
Language: Java
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small

28. Darwin: Web Page: http://www.mpi-sb.mpg.de/~baumgart/DARWIN/
E-Mail: baumgart@mpi-sb.mpg.de
Architect: Alexander Fuchs
Language: Objective CAML
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

29. DCTP: Web Page: http://www4.in.tum.de/~stenzg/
E-Mail: stenzg@mpi-sb.mpg.de
Architect: Gernot Stenz
Language: Scheme
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

30. Declare: Web Page: http://research.microsoft.com/~dsyme/declare.aspx
E-Mail: dsyme@microsoft.com
Architect: Don Syme
Language: Objective CAML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

31. DITLU: Web Page: http://www.dcs.qmul.ac.uk/~uhmm/info/caar.html
E-Mail: aaa@cs.st-andrews.ac.uk
Architect: Andrew Adams
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: Classical, Size: Small

32. DN: Web Page: http://bailhache.humana.univ-nantes.fr/dnfn/deductioneng.html
E-Mail: patrice.bailhache@humana.univ-nantes.fr
Architect: Patrice Bailhache
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small

33. Doris: Web Page: http://www.coli.uni-saarland.de/~bos/atp/doris-info.html
E-Mail: bos@coli.uni-sb.de
Architect: Johan Bos
Language: Prolog
Category: Theorem Prover
Interaction: Batch, Logic: Classical, Size: Small

34. DOVE: Isabelle: Web Page: http://www.dsto.defence.gov.au/esrl/itd/dove
E-Mail: Tony.Cant@dsto.defence.gov.au
Architect: Tony Cant
Language: Tcl
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small

35. DReaM: Web Page: http://dream.inf.ed.ac.uk/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown

36. E: Web Page: http://www.eprover.org/
E-Mail: schulz@informatik.tu-muenchen.de
Architect: Stephan Schulz
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

37. EHDM: Web Page: http://www.csl.sri.com/users/rushby/
E-Mail: Unknown
Architect: John Rushby, Sam Owre
Language: Lucid Common Lisp
Category: Specification Environment
Interaction: Dialog, Logic: Classical, Size: Small

38. EPGY: Web Page: http://epgy.stanford.edu/TPE/
E-Mail: epgy-admin@epgy.stanford.edu
Architect: Rick Sommer, Pat Suppes
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Classical, Size: Small

39. EQP: Web Page: http://www-unix.mcs.anl.gov/AR/eqp/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

40. ERA: Web Page: http://www.eecs.ku.edu/faculty_staff/bio/faculty/andygill
E-Mail: Unknown
Architect: Andy Gill
Language: Haskell
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Small

41. EVES: Web Page: http://www.springerlink.com/content/p225421w45016110/
E-Mail: Unknown
Architect: Sentot Kromodimoeljo, Irwin Meisels, Mark Saaltink, Bill Pase, Dan Craigen
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Commercial

42. Expander2: Web Page: http://fldit-www.cs.uni-dortmund.de/~peter/
E-Mail: peter.padawitz@udo.edu
Architect: Peter Padawitz
Language: O'Haskell
Category: Theorem Prover
Interaction: Editor, Logic: Classical, Size: Small

43. FDPLL: Web Page: http://www.uni-koblenz.de/~peter/FDP/
E-Mail: peter@uni-koblenz.de
Architect: Peter Baumgartner
Language: Eclipse Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

44. Finder: Web Page: http://users.rsise.anu.edu.au/~jks/finder.html
E-Mail: Unknown
Architect: John Slaney
Language: C
Category: First Order Prover
Interaction: Batch, Logic: Classical, Size: Small

45. Fitch, Boole, Tarski's World, Grade Grinder: Web Page: http://www-csli.stanford.edu/LPL/
E-Mail: Unknown
Architect: John Barwise, John Etchemendy, Gerard Allwein, Dave Barker-Plummer, Albert Liu
Language: Java, C
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Commercial

46. Funmath: Web Page: http://www.funmath.be/
E-Mail: boute@intec.UGent.be
Architect: Raymond Boute
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Classical, Size: Small

47. Getfol: Web Page: http://www.cs.unitn.it/~getfol/startgwigb.html
E-Mail: Unknown
Architect: Fausto Giunchiglia
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

48. Ghilbert: Web Page: http://www.ghilbert.org/
E-Mail: raph@acm.org
Architect: Raph Levien
Language: Python
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

49. Goedel: Web Page: http://www.math.gatech.edu/~belinfan/research/autoreas/
E-Mail: belinfan@math.gatech.edu
Architect: Johan Belinfante
Language: Mathematica
Category: Theorem Prover
Interaction: Editor, Logic: Classical, Size: Small

50. HLM: Web Page: http://hlm.sourceforge.net/
E-Mail: SebastianR@gmx.de
Architect: Sebastian Reichelt
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

51. HOL: HOL Light: Web Page: http://www.cl.cam.ac.uk/~jrh13/hol-light/
E-Mail: johnh@ichips.intel.com
Architect: John Harrison
Language: CAML Light
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small

52. HOL: HOL98: Web Page: http://www.cl.cam.ac.uk/research/hvg/HOL/
E-Mail: Unknown
Architect: Konrad Slind, e.a.
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Large

53. Hyperproof: Web Page: http://www-csli.stanford.edu/hp/index.html#Hyperproof
E-Mail: Unknown
Architect: Gerry Allwein, Mark Greaves, Mike Lenz
Language: C, Pascal, Assembly
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Large

54. ICS: Web Page: http://www.icansolve.com/
E-Mail: ruess@csl.sri.com
Architect: Jean-Christophe Filliâtre
Language: Objective CAML
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

55. IMPS: Web Page: http://imps.mcmaster.ca/
Mailing List: imps-request@imps.mcmaster.ca
Architect: W.M. Farmer, J.D. Guttman, F.J. Thayer
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

56. INKA: Web Page: http://www.dfki.de/vse/systems/inka/
E-Mail: Unknown
Architect: Dieter Hutter
Language: Lucid Common Lisp
Category: Theorem Prover
Interaction: Editor, Logic: Classical, Size: Small

57. Isabelle: TAS, IsaWin: Web Page: http://www.informatik.uni-bremen.de/~cxl/tas/home.html
E-Mail: cxl@informatik.uni-bremen.de
Architect: Christoph Lüth, Burkhart Wolff
Language: Standard ML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

58. Ivy: Web Page: http://www.cs.unm.edu/~mccune/papers/ivy/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune, Olga Shumsky
Language: ACL2
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

59. Kimba: Web Page: http://www.ags.uni-sb.de/~konrad/kimba.html
E-Mail: konrad@ags.uni-sb.de
Architect: Karsten Konrad
Language: Oz
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

60. Larch: LP: Web Page: http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html
E-Mail: Unknown
Architect: Stephen Garland, John Guttag
Language: CLU
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

61. Larch: LSL: Web Page: http://www.sds.lcs.mit.edu/spd/larch/lsl.html
E-Mail: Unknown
Architect: Stephen Garland, John Guttag
Language: CLU
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Large

62. leanTAP: Web Page: http://i12www.ira.uka.de/leantap/
E-Mail: beckert@ira.uka.de
Architect: Bernhard Beckert, Joachim Posegga
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

63. Leo: Web Page: http://www.ags.uni-sb.de/~omega/www/leo.html
E-Mail: chris@ags.uni-sb.de
Architect: Christoph Benzmüller
Language: Common Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

64. LogicCoach 9: Web Page: http://academic.csuohio.edu/polen/
E-Mail: n.pole@csuohio.edu
Architect: Nelson Pole
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small

65. LogicWorks: Web Page: http://www.bgsu.edu/pdc/logicwo.html
E-Mail: lechar@bgnet.bgsu.edu
Architect: Rob Brady
Language: Unknown
Category: Logic Education
Interaction: Dialog, Logic: Classical, Size: Commercial

66. Mace: Web Page: http://www-unix.mcs.anl.gov/AR/mace/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

67. Marcel: Web Page: http://math.boisestate.edu/~holmes/proverpage.html
E-Mail: holmes@math.boisestate.edu
Architect: M. Randall Holmes
Language: Standard ML
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

68. MathScheme: Web Page: http://imps.mcmaster.ca/mathscheme/
E-Mail: wmfarmer@mcmaster.ca
Architect: William M. Farmer, Martin v. Mohrenschildt
Language: Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Classical, Size: Small

69. MathXpert: Web Page: http://www.HelpWithMath.com/
E-Mail: feedback@HelpWithMath.com
Architect: Michael Beeson
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: Classical, Size: Commercial

70. Metamath: Web Page: http://metamath.org/
E-Mail: nm@alum.mit.edu
Architect: Norman Megill
Language: C
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

71. METEOR: Web Page: http://www.cs.duke.edu/~ola/meteor.html
E-Mail: ola@cs.duke.edu
Architect: Owen Astrachan
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

72. Mizar: Web Page: http://www.mizar.org/
E-Mail: romat@mizar.org
Architect: Andrzej Trybulec, Czeslaw Bylinski
Language: Free Pascal
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Large

73. Mural: Web Page: http://www.cis.rl.ac.uk/proj/mural.html
E-Mail: Unknown
Architect: Brian Ritchie
Language: Unknown
Category: Specification Environment
Interaction: Editor, Logic: Classical, Size: Small

74. Nqthm: Web Page: ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html
Mailing List: nqthm-users@cs.utexas.edu
Architect: Bob Boyer, J. Strother Moore, e.a.
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

75. Nqthm: PC-Nqthm: Web Page: http://www.computationallogic.com/software/pc-nqthm/index.html
E-Mail: Unknown
Architect: Matt Kaufman
Language: Common Lisp
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Unknown

76. Omega: Web Page: http://www.ags.uni-sb.de/~omega/
E-Mail: kohlhase@ags.uni-sb.de
Architect: Michael Kohlhase
Language: Common Lisp, CLOS
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

77. Ontic: Web Page: http://www-cgi.cs.cmu.edu./afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html
E-Mail: ontic-implementors@ai.mit.edu
Architect: David McAllester
Language: Common Lisp
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Small

78. OpenProof: Web Page: http://www-vil.cs.indiana.edu/hwc4.html
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Unknown

79. OSHL: Web Page: http://www.cs.unc.edu/~plaisted/
E-Mail: zhu@cs.unc.edu
Architect: Yunshan Zhu, David Plaisted
Language: ECLiPSe Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

80. Otter: Web Page: http://www-unix.mcs.anl.gov/AR/otter/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Large

81. Paradox: Web Page: http://www.cs.chalmers.se/~koen/paradox/
E-Mail: koen@cs.chalmers.se
Architect: Koen Claessen, Niklas Sörensson
Language: Haskell, C++
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

82. Peers: Web Page: http://www.cs.uiowa.edu/~bonacina/cd.html
E-Mail: bonacina@cs.uiowa.edu
Architect: Maria Paola Bonacina
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

83. ProCom: Web Page: ftp://www.koralle.imn.htwk-leipzig.de/pub/ProCom/procom.html
E-Mail: Unknown
Architect: Gerd Neugebauer
Language: ECLiPSe Prolog
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

84. ProofCheck: Web Page: http://www.proofcheck.org/
E-Mail: neveln@cs.widener.edu
Architect: Bob Neveln
Language: Python
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

85. ProofPower: Web Page: http://www.lemma-one.com/ProofPower/index/
E-Mail: rda@lemma-one.com
Architect: Rob Arthan, Roger Bishop Jones
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Large

86. Proof Tutor: Web Page: http://hss.cmu.edu/html/departments/philosophy/Proof_Tutor.html
E-Mail: R.Scheines@andrew.cmu.edu
Architect: Wilfried Sieg, Richard Scheines
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small

87. PROTEIN: Web Page: http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/
E-Mail: peter@uni-koblenz.de
Architect: Peter Baumgartner
Language: ECLiPSe Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

88. ProveEasy: Web Page: http://www.dcs.ed.ac.uk/home/rb/
E-Mail: rb@dcs.ed.ac.uk
Architect: Rod Burstall
Language: Tcl
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

89. Prover9: Web Page: http://www.cs.unm.edu/~mccune/prover9/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

90. Prover, NP-Tools: Web Page: http://www.prover.com/
E-Mail: Unknown
Architect: Graeme Parkin, Gunnar Stalmarck
Language: C
Category: Theorem Prover
Interaction: Library, Logic: Classical, Size: Commercial

91. PTTP: Web Page: http://www.ai.sri.com/~stickel/pttp.html
E-Mail: stickel@ai.sri.com
Architect: Mark Stickel
Language: Common Lisp, Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

92. Purr: Web Page: http://www-cad.eecs.berkeley.edu/~cm/publications/mt/
E-Mail: cm@eecs.berkeley.edu
Architect: Christoph Meyer
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

93. PVS: Web Page: http://pvs.csl.sri.com/
Mailing List: pvs-help@csl.sri.com
Architect: Sam Owre, Natarajan Shankar
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Commercial

94. qedeq: Hilbert II: Web Page: http://www.qedeq.org/
E-Mail: mime@qedeq.org
Architect: Michael Meyling
Language: Java
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small

95. QuodLibet: Web Page: http://agent.informatik.uni-kl.de/quodlibet.html
E-Mail: schmidt@informatik.uni-kl.de
Architect: Ulrich Kuehler, Tobias Schmidt-Samoa, Claus-Peter Wirth
Language: Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

96. RRL: Web Page: file://cs.uiowa.edu/pub/hzhang/rrl/
E-Mail: Unknown
Architect: Hantao Zhang
Language: Zeta Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

97. Satchmo: Web Page: http://www.pms.ifi.lmu.de/software/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

98. Saturate: Web Page: http://www.mpi-sb.mpg.de/SATURATE/
E-Mail: Unknown
Architect: Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

99. Scott: Web Page: http://users.rsise.anu.edu.au/~jks/scott.html
E-Mail: John.Slaney@anu.edu.au
Architect: John Slaney
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

100. SETHEO: Web Page: http://wwwjessen.informatik.tu-muenchen.de/~setheo/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Unknown

101. Simplify: Web Page: http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html
E-Mail: gnelson@pa.dec.com
Architect: Dave Detlefs, Greg Nelson, Jim Saxe
Language: Modula-3
Category: Theorem Prover
Interaction: Batch, Logic: Classical, Size: Small

102. Smiley: Web Page: http://www.mpi-sb.mpg.de/~nivelle/
E-Mail: nivelle@mpi-sb.mpg.de
Architect: Hans de Nivelle
Language: C++
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

103. Snark: Web Page: http://www.ai.sri.com/~stickel/snark.html
E-Mail: stickel@ai.sri.com
Architect: Mark Stickel
Language: Common Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

104. Sparkle: Web Page: http://www.cs.kun.nl/Sparkle/
E-Mail: maartenm@cs.kun.nl
Architect: Maarten de Mol
Language: Clean
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small

105. SPASS: Web Page: http://www.mpi-sb.mpg.de/units/ag2/projects/SPASS/
E-Mail: Unknown
Architect: Christoph Weidenbach
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Unknown

106. SPL: Web Page: http://www.cs.kent.ac.uk/pubs/1999/909/
E-Mail: vince@sharp.co.uk
Architect: Vincent Zammit
Language: Standard ML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small

107. SPRFN: Web Page: http://www.cs.unc.edu/Research/mi/mi-provers.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

108. SPTHEO: Web Page: http://wwwjessen.informatik.tu-muenchen.de/~suttner/sptheo.html
E-Mail: Unknown
Architect: Christian Suttner
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

109. SymLog: Web Page: http://www.symlog.ca/Profile/Fred.htm
E-Mail: tully@chass.utoronto.ca
Architect: Frederic Portoraro
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small

110. Tableau3: Web Page: http://logic.philosophy.ox.ac.uk/
E-Mail: floridi@ermine.ox.ac.uk
Architect: Luciano Floridi
Language: Unknown
Category: Logic Education
Interaction: Dialog, Logic: Classical, Size: Small

111. Tableaux: Web Page: http://www-formal.stanford.edu/clt/ARS/Entries/tableaux
E-Mail: Unknown
Architect: Ron Burback
Language: Unknown
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Unknown

112. Techs: Teamwork: Web Page: http://www-avenhaus.informatik.uni-kl.de/mitarbeiter/denzinger/cooperation.html
E-Mail: denzinge@informatik.uni-kl.de
Architect: Jörg Denzinger
Language: Unknown
Category: Theorem Prover
Interaction: Script, Logic: Classical, Size: Small

113. Tecton: Web Page: http://www.cs.rpi.edu/~musser/Tecton/
E-Mail: musser@cs.rpi.edu
Architect: David Musser, Deepak Kapur
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Classical, Size: Small

114. The Logic Daemon: Web Page: http://logic.tamu.edu/daemon.html
E-Mail: colin-allen@tamu.edu
Architect: Colin Allen
Language: Perl, C
Category: Logic Education
Interaction: Batch, Logic: Classical, Size: Small

115. Theorema: Web Page: http://www.risc.uni-linz.ac.at/research/theorema/description/
E-Mail: theorema@theorema.org
Architect: Bruno Buchberger
Language: Mathematica
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large

116. TPS: Web Page: http://gtps.math.cmu.edu/tps.html
E-Mail: Peter.Andrews@cmu.edu
Architect: Peter Andrews
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

117. TPTP: Web Page: http://wwwjessen.informatik.tu-muenchen.de/~tptp/
E-Mail: Unknown
Architect: Geoff Sutcliffe, Christian Suttner
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown

118. Universal Math Solver: Web Page: http://www.umsolver.com/
E-Mail: norths@mail.rcom.ru
Architect: Stanislav Kublanovsky
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: Classical, Size: Small

119. Vampire: Web Page: http://en.wikipedia.org/wiki/Vampire_theorem_prover
E-Mail: riazanov@cs.man.ac.uk
Architect: Andrei Voronkov, Alexandre Riazanov
Language: C++
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

120. Waldmeister: Web Page: http://www.waldmeister.org/
E-Mail: waldmeister@informatik.uni-kl.de
Architect: Arnim Buch, Thomas Hillenbrand
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small

121. Watson: Web Page: http://math.boisestate.edu/~holmes/proverpage.html
E-Mail: holmes@math.boisestate.edu
Architect: M. Randall Holmes
Language: Standard ML
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small

122. Weierstrass: Web Page: http://www.mathcs.sjsu.edu/faculty/beeson/Papers/weier.html
E-Mail: beeson@mathcs.sjsu.edu
Architect: Michael Beeson
Language: C
Category: Theorem Prover
Interaction: Script, Logic: Classical, Size: Small

123. Z: Fuzz: Web Page: http://spivey.oriel.ox.ac.uk/mike/fuzz/
E-Mail: mike@comlab.ox.ac.uk
Architect: Mike Spivey
Language: C
Category: Representation
Interaction: Interface, Logic: Classical, Size: Large

Constructive

124. Agda: Web Page: http://www.cs.chalmers.se/~catarina/agda/
E-Mail: Unknown
Architect: Catarina Coquand
Language: Haskell
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Small

125. Coq: Web Page: http://coq.inria.fr/
Mailing List: coq-club@inria.fr
Architect: Gérard Huet, Chet Murthy, e.a.
Language: Objective CAML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Large

126. Coq: CtCoq: Web Page: http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html
E-Mail: ctcoq-request@sophia.inria.fr
Architect: Yves Bertot, e.a.
Language: Unknown
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

127. Epigram: Web Page: http://www.dur.ac.uk/CARG/epigram/
E-Mail: c.t.mcbride@durham.ac.uk
Architect: Conor McBride
Language: Haskell
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Small

128. FT: Web Page: http://www.sm.luth.se/~torkel/eget/ftinfo.html
E-Mail: torkel@sm.luth.se
Architect: Torkel Franzén
Language: C
Category: First Order Prover
Interaction: Script, Logic: Constructive, Size: Small

129. Half: C-Half: Web Page: http://www.dcs.ed.ac.uk/home/pgh/half.html
E-Mail: Unknown
Architect: Dan Synek
Language: C
Category: Proof Checker
Interaction: Editor, Logic: Constructive, Size: Small

130. Henk: Web Page: http://www.cse.ogi.edu/~erik/Personal/typed.htm
E-Mail: erik@cse.ogi.edu
Architect: Simon Peyton Jones, Erik Meijer
Language: Haskell
Category: Representation
Interaction: Interface, Logic: Constructive, Size: Small

131. Int: Web Page: http://class-int.narod.ru
E-Mail: urchick@mail.ru
Architect: Yuri Vtorushin, Oleg Okhotnikov
Language: C++
Category: Proof Checker
Interaction: Batch, Logic: Constructive, Size: Small

132. KIV: Web Page: http://i11www.iti.uni-karlsruhe.de/~kiv/KIV-KA.html
E-Mail: kiv-team@ira.uka.de
Architect: Unknown
Language: Lucid Common Lisp
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

133. Kripke: Web Page: http://arp.anu.edu.au:80/ftp/kripke/
E-Mail: Unknown
Architect: Gustav Meglicki
Language: Pascal
Category: First Order Prover
Interaction: Script, Logic: Constructive, Size: Small

134. Lambda: Web Page: http://www.cis.ksu.edu/~stough/lambda.html
E-Mail: allen@cis.ksu.edu
Architect: Allen Stoughton
Language: C
Category: Theorem Prover
Interaction: Script, Logic: Constructive, Size: Small

135. lambda Clam: Web Page: http://dream.inf.ed.ac.uk/software/lambda-clam/
E-Mail: jjb@dai.ed.ac.uk
Architect: Unknown
Language: Teyjus lambda Prolog
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

136. lambda Prolog: Web Page: http://www.cse.psu.edu/~dale/lProlog/
E-Mail: Unknown
Architect: Dale Miller
Language: C
Category: Specification Environment
Interaction: Unknown, Logic: Constructive, Size: Small

137. Lego: Web Page: http://www.dcs.ed.ac.uk/home/lego/
E-Mail: Unknown
Architect: Randy Pollack
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Large

138. Matita: Web Page: http://matita.cs.unibo.it/
Mailing List: matita-user@cs.unibo.it
Architect: Claudio Sacerdoti Coen, Andrea Asperti
Language: Objective CAML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

139. MetaPRL: Web Page: http://metaprl.org/default.html
E-Mail: metaprl@metaprl.org
Architect: Jason Hickey, Aleksey Nogin
Language: Objective CAML
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Large

140. Minlog: Web Page: http://www.mathematik.uni-muenchen.de/~minlog/
E-Mail: schwicht@rz.mathematik.uni-muenchen.de
Architect: Helmut Schwichtenberg
Language: Scheme
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

141. Nuprl: Web Page: http://www.cs.cornell.edu/Info/Projects/NuPrl/
E-Mail: nuprl@cs.cornell.edu
Architect: Joseph Bates, Robert Constable, Stuart Allen, Douglas Howe, e.a.
Language: ML, Common Lisp
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Large

142. Oleg: Web Page: http://www.dcs.ed.ac.uk/home/ctm/oleg/quiet/
E-Mail: ctm@dcs.ed.ac.uk
Architect: Conor McBride
Language: ML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

143. PhoX: Web Page: http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html
Mailing List: af2@logique.jussieu.fr
Architect: Christophe Raffalli
Language: Objective CAML
Category: Tactic Prover
Interaction: Script, Logic: Constructive, Size: Small

144. Plastic: Web Page: http://www.dur.ac.uk/CARG/plastic.html
E-Mail: P.C.Callaghan@durham.ac.uk
Architect: Paul Callaghan
Language: Haskell
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

145. Porgi: Web Page: http://www.cis.ksu.edu/~stough/porgi.html
E-Mail: allen@cis.ksu.edu
Architect: Allen Stoughton
Language: Standard ML of New Jersey
Category: Theorem Prover
Interaction: Script, Logic: Constructive, Size: Small

146. Proof: Web Page: http://www.keyfitz.org/jburdick/
E-Mail: jburdick@gradient.cis.upenn.edu
Architect: Josh Burdick
Language: Java
Category: Proof Checker
Interaction: Script, Logic: Constructive, Size: Small

147. Tutch: Web Page: http://www.tcs.informatik.uni-muenchen.de/~abel/tutch/
E-Mail: abel@informatik.uni-muenchen.de
Architect: Andreas Abel
Language: Standard ML of New Jersey
Category: Proof Checker
Interaction: Batch, Logic: Constructive, Size: Small

148. Typelab: Web Page: http://www.informatik.uni-ulm.de/ki/typelab.html
E-Mail: luther@informatik.uni-ulm.de
Architect: Martin Strecker, Marko Luther
Language: Common Lisp
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

149. Yarrow: Web Page: http://www.cs.ru.nl/~janz/yarrow/
E-Mail: janz@cs.kun.nl
Architect: Jan Zwanenburg
Language: Haskell
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small

None

150. Axiom: Web Page: http://www.axiom-developer.org
E-Mail: daly@axiom-developer.org
Architect: Richard Jenks, Robert Sutor
Language: Common Lisp, C, Boot, Spad
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

151. bc: Web Page: http://www.gnu.org/software/bc/
E-Mail: Unknown
Architect: Unknown
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

152. calc: Web Page: http://www.numbertheory.org/calc/krm_calc.html
E-Mail: krm@maths.uq.edu.au
Architect: Unknown
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

153. Cocoa: Web Page: http://cocoa.dima.unige.it/
E-Mail: cocoa@dima.unige.it
Architect: Antonio Capani, Gianfranco Niesi
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

154. CREP: Web Page: http://www.mathematik.uni-bielefeld.de/~sek/crep.html
E-Mail: fdowner@mathematik.uni.bielefeld.de
Architect: Peter Dräxler
Language: Pascal, C, Java, Maple
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

155. Derive: Web Page: http://en.wikipedia.org/wiki/Derive_computer_algebra_system
E-Mail: Unknown
Architect: David Stoutemyer, Albert Rich
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

156. Equplus: Web Page: http://equplus.net/
E-Mail: Unknown
Architect: Maria Chernenko
Language: Unknown
Category: Information
Interaction: Corpus, Logic: None, Size: Small

157. Expressionist: Web Page: http://www.livemath.com/matheq/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial

158. Fermat: Web Page: http://www.bway.net/~lewis/
E-Mail: rlewis@fordham.edu
Architect: Robert Lewis
Language: Pascal
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

159. Form: Web Page: http://www.nikhef.nl/~form/
E-Mail: Unknown
Architect: Jos Vermaseren
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

160. FriCAS: Web Page: http://fricas.sourceforge.net/
E-Mail: fricas-devel@googlegroups.com
Architect: Richard Jenks, Robert Sutor
Language: Common Lisp, C, Boot, Spad
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

161. Gb/FGb, RS: Web Page: http://fgbrs.lip6.fr/
E-Mail: jcf@calfor.lip6.fr
Architect: Jean-Charles Faugère
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: None, Size: Small

162. Giac/xcas: Web Page: http://www-fourier.ujf-grenoble.fr/~parisse/english.html
E-Mail: parisse@fourier.ujf-grenoble.fr
Architect: Bernard Parisse
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

163. GiNaC: Web Page: http://www.ginac.de/
Mailing List: ginac-list@ginac.de
Architect: Christian Bauer, Alexander Frink, Richard Kreckel
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

164. HDM: Web Page: http://wiki.planetmath.org/AsteroidMeta/HDM
E-Mail: holtzermann17@gmail.com
Architect: Joe Corneli
Language: Lisp
Category: Representation
Interaction: Script, Logic: None, Size: Small

165. JACAL: Web Page: http://swiss.csail.mit.edu/~jaffer/JACAL
E-Mail: agj@alum.mit.edu
Architect: Aubrey Jaffer
Language: Scheme
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

166. JavaMath: Web Page: http://javamath.sourceforge.net/
E-Mail: javamath-support@lists.sourceforge.net
Architect: Andrew Solomon, Craig Struble
Language: Java
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

167. KANT/KASH: Web Page: http://www.math.tu-berlin.de/~kant/kash.html
E-Mail: kant@math.tu-berlin.de
Architect: Michael Pohst
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

168. Leda: Web Page: http://www.mpi-sb.mpg.de/LEDA/
E-Mail: Unknown
Architect: Stefan Näher
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Unknown

169. LiDIA: Web Page: http://www.cdc.informatik.tu-darmstadt.de/TI/LiDIA/
Mailing List: LiDIA-request@cdc.informatik.tu-darmstadt.de
Architect: Unknown
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

170. LiveMath: Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

171. LLF: Web Page: http://theory.stanford.edu/~iliano/LLF/LLF.html
E-Mail: iliano@cs.stanford.edu
Architect: Iliano Cervesato
Language: ML
Category: Proof Checker
Interaction: Batch, Logic: None, Size: Small

172. Macaulay: Web Page: http://www.math.uiuc.edu/Macaulay2/
E-Mail: Unknown
Architect: Daniel Grayson, Michael Stillman
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Unknown

173. Macsyma: Web Page: http://www.macsyma.com/
E-Mail: Unknown
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

174. Macsyma: Maxima: Web Page: http://maxima.sourceforge.net/
Mailing List: maxima@math.utexas.edu
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

175. Macsyma: Punimax: Web Page: http://symbolicnet.mcs.kent.edu/systems/macsyma.html
E-Mail: Unknown
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

176. Magma: Web Page: http://magma.maths.usyd.edu.au/
E-Mail: magma@maths.usyd.edu.au
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Script, Logic: None, Size: Commercial

177. Maple: Web Page: http://www.maplesoft.com/
E-Mail: sales_info@maplesoft.com
Architect: Keith Geddes, Gaston Gonnet, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

178. Mathcad: Web Page: http://www.mathcad.com/mathcad/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

179. Mathematica: Web Page: http://www.wolfram.com/products/mathematica/index.html
E-Mail: info@wolfram.com
Architect: Stephen Wolfram, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

180. Mathematica: Publicon: Web Page: http://www.wolfram.com/products/publicon/index.html
E-Mail: info@publicon.com
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial

181. MathScript: Web Page: http://www.mathscript.pair.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial

182. MathView: Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

183. Merill: Web Page: ftp://ftp.dcs.glasgow.ac.uk/pub/merill/
E-Mail: Unknown
Architect: Brian Matthews
Language: Standard ML
Category: Specification Environment
Interaction: Dialog, Logic: None, Size: Small

184. MuPAD: Web Page: http://www.mupad.de/
E-Mail: Unknown
Architect: Benno Fuchssteiner, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

185. nauty: Web Page: http://cs.anu.edu.au/~bdm/nauty/
E-Mail: bdm@cs.anu.edu.au
Architect: Brendan D. McKay
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

186. NTL: Web Page: http://www.cs.wisc.edu/~shoup/ntl/
E-Mail: shoup@cs.wisc.edu
Architect: Victor Shoup
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

187. OpenMath: Web Page: http://www.openmath.org/
E-Mail: Unknown
Architect: Gaston Gonnet
Language: SGML
Category: Representation
Interaction: Interface, Logic: None, Size: Small

188. Pari/GP: Web Page: http://pari.math.u-bordeaux.fr/
E-Mail: pari@math.u-bordeaux.fr
Architect: Henri Cohen
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

189. polymake: Web Page: http://www.math.tu-berlin.de/polymake/
E-Mail: polymake@math.tu-berlin.de
Architect: Ewgenij Gawrilow, Michael Joswig
Language: C++
Category: Computer Algebra
Interaction: Script, Logic: None, Size: Small

190. Reduce: Web Page: http://www.uni-koeln.de/REDUCE/
E-Mail: Unknown
Architect: Tony Hearn
Language: Standard Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial

191. ring.perisic.com: Web Page: http://ring.perisic.com/
E-Mail: marc@pension-perisic.de
Architect: Marc Conrad
Language: Java
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

192. Rotater: Web Page: http://casr.adelaide.edu.au/rotater/
E-Mail: craig@raru.adelaide.edu.au
Architect: Craig Kloeden
Language: C
Category: Computer Algebra
Interaction: Editor, Logic: None, Size: Small

193. SACLIB: Web Page: http://www.cis.udel.edu/~saclib/
Mailing List: saclib-l@risc.uni-linz.ac.at
Architect: George E. Collins, Hoon Hong
Language: C
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

194. Schoonschip: Web Page: ftp://archive.umich.edu/physics/schip/
E-Mail: Unknown
Architect: Martin Veltman
Language: 68000 Assembly
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

195. Scilab: Web Page: http://www.scilab.org/
E-Mail: Unknown
Architect: Unknown
Language: C, Fortran
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large

196. Singular: Web Page: http://www.singular.uni-kl.de/
E-Mail: singular@mathematik.uni-kl.de
Architect: Unknown
Language: C, C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

197. Swift: Web Page: http://www.geocities.com/SiliconValley/Heights/5445/survey.html
E-Mail: Unknown
Architect: P S Karthikeyan, P S Ranganathan
Language: Java
Category: Authoring
Interaction: Editor, Logic: None, Size: Small

198. SYNAPS: Web Page: http://www-sop.inria.fr/galaad/logiciels/synaps/
E-Mail: mourrain@sophia.inria.fr
Architect: Unknown
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small

199. Techexplorer: Web Page: http://www.software.ibm.com/network/techexplorer/
E-Mail: techexpl@us.ibm.com
Architect: Robert Sutor, Angel Diaz
Language: C++
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial

200. TeX: LaTeX: Web Page: http://www.tug.org/
E-Mail: Unknown
Architect: Donald Knuth, Leslie Lamport
Language: Pascal
Category: Authoring
Interaction: Script, Logic: None, Size: Large

201. Twelf: Web Page: http://www.cs.cmu.edu/~twelf/
Mailing List: elf-list-request@cs.cmu.edu
Architect: Frank Pfenning, Carsten Schürmann
Language: Standard ML
Category: Proof Checker
Interaction: Batch, Logic: None, Size: Large

202. Yacas: Web Page: http://yacas.sourceforge.net/
E-Mail: Unknown
Architect: Ayal Pinkus
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small

Unknown

203. Acela: Web Page: http://homepages.cwi.nl/~steven/acela/
E-Mail: steven@cwi.nl
Architect: Arjeh Cohen, Lambert Meertens
Language: HTML
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small

204. ActiveMath: Web Page: http://www.mathweb.org/activemath/
E-Mail: melis@ags.uni-sb.de
Architect: Erica Melis
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

205. Aldor: Web Page: http://www.aldor.org/
E-Mail: Stephen.Watt@sophia.inria.fr
Architect: Stephen Watt
Language: C
Category: Computer Algebra
Interaction: Batch, Logic: Unknown, Size: Small

206. Amphion: Web Page: http://ase.arc.nasa.gov/docs/amphion.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

207. B Method: Atelier B: Web Page: http://www.atelierb.societe.com/
E-Mail: maintenance.atelierb@clearsy.com
Architect: Jean-Raymond Abrial
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial

208. B Method: B4free: Web Page: http://www.b4free.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

209. B Method: Click'n'Prove: Web Page: http://www.loria.fr/~cansell/cnp.html
E-Mail: cansell@lloria.fr
Architect: Jean-Raymond Abrial, Dominique Cansell
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

210. CafeOBJ: Web Page: http://www.ldl.jaist.ac.jp/cafeobj/
E-Mail: Unknown
Architect: Kokichi Futatsugi
Language: Common Lisp
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

211. Calculemus: Web Page: http://www.mathweb.org/calculemus/
Mailing List: calculemus-ig@ags.uni-sb.de
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

212. CASL: Web Page: http://www.cofi.info/CASL.html
E-Mail: pdmosses@brics.dk
Architect: Michel Bidoit, Peter D. Mosses
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

213. Caveat: Web Page: http://www-list.cea.fr/gb/programmes/sys_embarques/labo_lsl/caveat/index_caveat_gb.htm
E-Mail: Jacques.Raguideau@cea.fr
Architect: Unknown
Language: C, C++
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial

214. CCR: RDL: Web Page: http://www.mrg.dist.unige.it/ccr/
E-Mail: silvio@dist.unige.it
Architect: Alessandro Armando, Silvio Ranise
Language: SICStus Prolog
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small

215. CL: Web Page: http://www.ii.fmph.uniba.sk/~voda/cl.html
E-Mail: voda@fmph.uniba.sk
Architect: Paul Voda
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small

216. Coral: Web Page: http://dream.inf.ed.ac.uk/projects/coral/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

217. Deduktion: Web Page: http://www.uni-koblenz.de/ag-ki/Deduktion/
E-Mail: peter@informatik.uni-koblenz.de
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

218. Deva: Devil: Web Page: http://swt.cs.tu-berlin.de/~ma/devil/index.html
E-Mail: ma@first.gmd.de
Architect: Matthias Anlauff
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small

219. DFG: Web Page: http://www.uni-koblenz.de/ag-ki/Deduktion/#OtherActivities
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

220. Dimacs: Web Page: ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.tex
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Unknown, Size: Small

221. Discount: Web Page: http://www.uni-kl.de/AG-AvenhausMadlener/discount.html
E-Mail: denzinge@informatik.uni-kl.de
Architect: Jörg Denzinger
Language: Unknown
Category: Theorem Prover
Interaction: Script, Logic: Unknown, Size: Small

222. DPL: CN D: Web Page: http://www.ai.mit.edu/projects/dynlangs/Projects/DPL.htm
E-Mail: koud@ai.mit.edu
Architect: Kostas Arkoudas
Language: ML
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small

223. DTP: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/dtp/0.html
E-Mail: Unknown
Architect: Don Geddis
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

224. ELAN: Web Page: http://www.loria.fr/equipes/protheo/PROJECTS/ELAN/elan.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Unknown

225. Ergo: Web Page: http://www.itee.uq.edu.au/~pjr/HomePages/ErgoHome.html
E-Mail: Unknown
Architect: Peter Robinson, e.a.
Language: Qu Prolog
Category: Tactic Prover
Interaction: Unknown, Logic: Unknown, Size: Small

226. Esterel: Web Page: http://www.esterel-technologies.com/
Mailing List: esterel-users@sophia.inria.fr
Architect: Gérard Berry
Language: Esterel
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

227. Evidence Algorithm: SAD: Web Page: http://ea.unicyb.kiev.ua/sad.en.html
E-Mail: lav@unicyb.kiev.ua
Architect: Andrey Paskevich
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small

228. Evolver: Web Page: http://www.susqu.edu/facstaff/b/brakke/evolver/evolver.html
E-Mail: brakke@susqu.edu
Architect: Ken Brakke
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small

229. EzMath: Web Page: http://www.w3.org/People/Raggett/EzMath/
E-Mail: Unknown
Architect: Dave Raggett
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small

230. Fiesta: Web Page: http://www.cs.miami.edu/~tptp/CASC/16/SystemDescriptions.html#Fiesta
E-Mail: roberto@lsi.upc.es
Architect: Robert Nieuwenhuis
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small

231. Focal: Web Page: http://focal.inria.fr/site/index.php
E-Mail: therese.hardin@lip6.fr
Architect: Thérèse Hardin, Renaud Rioboo
Language: Objective CAML
Category: Computer Algebra
Interaction: Library, Logic: Unknown, Size: Small

232. foetus: Web Page: http://www.informatik.uni-muenchen.de/~abel/publications/foetus/
E-Mail: abel@informatik.uni-muenchen.de
Architect: Andreas Abel
Language: Standard ML
Category: Specification Environment
Interaction: Batch, Logic: Unknown, Size: Small

233. FOL: Web Page: http://www-formal.stanford.edu/pub/FOL/home.html
E-Mail: rww@sail.stanford.edu
Architect: Richard Weyhrauch, Carolyn Talcott
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

234. Formal Methods Page: Web Page: http://www.onlinecomputersciencedegree.com/resources/formal-methods/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

235. Formal Methods Wiki: Web Page: http://formalmethods.wikia.com/
E-Mail: jonathan.bowen@lsbu.ac.uk
Architect: Jonathan Bowen
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

236. Forum: Web Page: http://www.lix.polytechnique.fr/Labo/Dale.Miller/forum/
E-Mail: Unknown
Architect: Dale Miller
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

237. Frapps: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/frapps/0.html
E-Mail: Unknown
Architect: Alan Frisch, Tomas Uribe, Michael Mitchell
Language: Common Lisp
Category: First Order Prover
Interaction: Unknown, Logic: Unknown, Size: Small

238. GAP: Web Page: http://www-gap.dcs.st-and.ac.uk/~gap/
E-Mail: gap@dcs.st-and.ac.uk
Architect: Martin Schönert, e.a.
Language: C
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Large

239. Geometry Expert: Web Page: http://en.wikipedia.org/wiki/Geometry_Expert
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

240. Graffiti: Web Page: http://www.math.uh.edu/~clarson/graffiti.html
E-Mail: MATH0@Jetson.UH.EDU
Architect: Siemion Fajtlowicz
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

241. Graph Theorist: Web Page: http://www.cs.hunter.cuny.edu/~epstein/html/gt.html
E-Mail: susan.epstein@hunter.cuny.edu
Architect: Susan Epstein
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

242. Guru: Web Page: http://code.google.com/p/guru-lang/
E-Mail: astump@acm.org
Architect: Aaron Stump
Language: Java
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

243. Helena: Web Page: http://helm.cs.unibo.it/lambda_delta/
E-Mail: fguidi@cs.unibo.it
Architect: Ferruccio Guidi
Language: Objective CAML
Category: Proof Checker
Interaction: Batch, Logic: Unknown, Size: Small

244. Helm: Web Page: http://helm.cs.unibo.it/
E-Mail: asperti@cs.unibo.it
Architect: Andrea Asperti
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

245. Hiper: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/hiper/0.html
E-Mail: Unknown
Architect: Jim Christian
Language: Common Lisp
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

246. HR: Web Page: http://www.dai.ed.ac.uk/daidb/people/homes/simonco/research/hr/
E-Mail: simonco@dai.ed.ac.uk
Architect: Simon Colton
Language: Unknown
Category: Theorem Prover
Interaction: Batch, Logic: Unknown, Size: Small

247. IDA: Algebra Interactive: Web Page: http://www.win.tue.nl/~ida/
E-Mail: Unknown
Architect: Arjeh Cohen, Hans Cuypers, Hans Sterk
Language: HTML
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small

248. ILF: Web Page: http://www.uni-koblenz.de/~dahn/index-Dateien/Page425.htm
E-Mail: ilfserv-request@mathematik.hu-berlin.de
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

249. IMP: Web Page: http://www.uclic.ucl.ac.uk/imp/
E-Mail: j.gow@ucl.ac.uk
Architect: Paul Cairns, Jeremy Gow
Language: XSL
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small

250. IPR: Web Page: http://www.cs.wcu.edu/~shults/FTP/IPR/
E-Mail: shults@cs.wcu.edu
Architect: Benjamin Shults
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

251. ISO 12083: Web Page: http://www.oasis-open.org/cover/gen-apps.html#iso12083DTDs
E-Mail: Unknown
Architect: Eric van Herwijnen
Language: SGML
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Unknown

252. ITP: Web Page: http://www.dcs.gla.ac.uk/~stuart/ITP/ITP.html
E-Mail: Unknown
Architect: Stuart Aitken, Tom Melham, Muffy Calder, Phil Gray
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

253. Keim: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/keim/0.html
E-Mail: Unknown
Architect: Dan Nesmith, Jörg Siekman
Language: Common Lisp, CLOS
Category: Theorem Prover
Interaction: Library, Logic: Unknown, Size: Unknown

254. KIDS: Web Page: http://www.kestrel.edu/home/prototypes/kids.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

255. Leibniz: Web Page: http://www.utdallas.edu/~klaus/Leibnizprogram/leibnizmain.html
E-Mail: klaus@utdallas.edu
Architect: Klaus Truemper
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small

256. llprover: Web Page: http://bach.seg.kobe-u.ac.jp/llprover/
E-Mail: tamura@kobe-u.ac.jp
Architect: Naoyuki Tamura
Language: SICStus Prolog
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small

257. Logic Animations: Web Page: http://turing.wins.uva.nl/~jaspars/animations/
E-Mail: jaspars@wins.uva.nl
Architect: Jan Jaspars
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Unknown, Size: Small

258. Logic Broker Architecture: Web Page: http://www.mathweb.org/calculemus/meetings/standrews00/armando.abstract
E-Mail: armando@mrg.dist.unige.it
Architect: Alessandro Armando, Daniele Zini
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

259. Logosphere: Web Page: http://www.logosphere.org/
Mailing List: logosphere-developer@cs.yale.edu
Architect: Carsten Schürmann
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

260. Map: Logiweb: Web Page: http://yoa.dk/
E-Mail: grue@diku.dk
Architect: Klaus Grue
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small

261. MathCaffeine: Web Page: http://atlas-conferences.com/c/a/e/e/48.htm
E-Mail: asvern@essex.ac.uk
Architect: Alexei Vernitski
Language: Unknown
Category: Authoring
Interaction: Unknown, Logic: Unknown, Size: Small

262. MathLive: Web Page: http://www.milohedge.com/products/mathlive/mathlive.html
E-Mail: info@milohedge.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial

263. MathML: Web Page: http://www.w3.org/Math/mathml-faq.html
E-Mail: Unknown
Architect: Unknown
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Unknown

264. MathPad: Web Page: http://pubpages.unh.edu/~mwidholm/MathPad/
E-Mail: Mark.Widholm@UNH.edu
Architect: Mark Widholm
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small

265. Mathtools: Web Page: http://www.mathtools.net/
E-Mail: feedback@mathtools.net
Architect: Ophir Herbst
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

266. MathWeb: Mosh: Web Page: http://www.mathweb.org/mathweb/
E-Mail: afranke@ags.uni-sb.de
Architect: Andreas Franke, Michael Kohlhase
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small

267. Matlab: Web Page: http://www.mathworks.com/products/matlab/
E-Mail: info@mathworks.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial

268. Maude: Web Page: http://maude.cs.uiuc.edu/
Mailing List: maude-users@maude.cs.uiuc.edu
Architect: José Meseguer
Language: Maude
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial

269. MBase: Web Page: http://www.mathweb.org/mbase/
E-Mail: kohlhase@cs.uni-sb.de
Architect: Andreas Franke, Michael Kohlhase
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Unknown, Size: Small

270. Minitab: Web Page: http://www.minitab.com/
E-Mail: sales@minitab.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial

271. MINSE: Web Page: http://lfw.org/math/
E-Mail: Unknown
Architect: Ka-Ping Yee
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small

272. MoWGLI: Web Page: http://www.mowgli.cs.unibo.it/
E-Mail: asperti@cs.unibo.it
Architect: Andrea Asperti
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

273. MuTTI: Web Page: http://www.tcs.informatik.uni-muenchen.de/mitarbeiter/alti/index.html
E-Mail: alti@informatik.uni-muenchen.de
Architect: Thorsten Altenkirch
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small

274. MVL: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/mvl/0.html
E-Mail: Unknown
Architect: Matthew Ginsberg
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

275. NewPandora: Web Page: http://www.doc.ic.ac.uk/~kb/#Pandora
E-Mail: kb@doc.ic.ac.uk
Architect: Krysia Broda
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Unknown, Size: Small

276. OMDoc: Web Page: http://www.mathweb.org/omdoc/
E-Mail: kohlhase+@cs.cmu.edu
Architect: Michael Kohlhase
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small

277. Omega: OAnts: Web Page: http://www.ags.uni-sb.de/~omega/index.php?target=publications&ref=C8
E-Mail: chris@ags.uni-sb.de
Architect: Christoph Benzmüller, Volker Sorge
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

278. OMRS: Web Page: http://www.kestrel.edu/home/people/coglio/ids98.ps
E-Mail: fausto@itc.it
Architect: Fausto Giunchiglia, Carolyn Talcott, Alessandro Armando
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small

279. OpenXM: Web Page: http://www.math.s.kobe-u.ac.jp/OpenXM/
E-Mail: takayama@math.sci.kobe-u.ac.jp
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small

280. ORA Canada Biblography of Automated Deduction: Web Page: http://www.ora.on.ca/biblio/biblio-prover-welcome.html
E-Mail: Unknown
Architect: Bill Pase, Karen Summerskill
Language: Unknown
Category: Information
Interaction: Corpus, Logic: Unknown, Size: Small

281. Oscar: Web Page: http://www.u.arizona.edu/~pollock/
E-Mail: Unknown
Architect: John Pollock
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

282. Perfect Developer: Web Page: http://www.eschertech.com/products/index.php
E-Mail: sales@eschertech.com
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial

283. Plural: Web Page: http://www.singular.uni-kl.de/plural/
E-Mail: Unknown
Architect: Gert-Martin Greuel, Viktor Levandovskyy, Hans Schönemann
Language: C, C++
Category: Computer Algebra
Interaction: Dialog, Logic: Unknown, Size: Small

284. ProofPad: Web Page: http://www-irm.mathematik.hu-berlin.de/~ilf/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

285. Prosper: Web Page: http://www.dcs.gla.ac.uk/prosper/
E-Mail: tfm@dcs.gla.ac.uk
Architect: T.F. Melham
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

286. QED Project: Web Page: http://www-unix.mcs.anl.gov/qed/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Interface, Logic: Unknown, Size: Small

287. QED Pro Quo: Web Page: http://www.qpq.org/
E-Mail: kohlhase+@cs.cmu.edu
Architect: Michael Kohlhase, Sam Owre, Natarajan Shankar
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small

288. REDLOG: Web Page: http://www.fmi.uni-passau.de/~redlog/
E-Mail: redlog@fmi.uni-passau.de
Architect: Andreas Dolzmann, Thomas Sturm
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

289. Risa/Asir: Web Page: http://www.asir.org/
E-Mail: takesima@flab.fujitsu.co.jp
Architect: Unknown
Language: C, Assembly
Category: Computer Algebra
Interaction: Dialog, Logic: Unknown, Size: Small

290. Safelogic Verifier: Web Page: http://www.jasper-da.com/products_jaspergold.htm
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

291. SEM: Web Page: http://www.cs.uiowa.edu/~hzhang/sem.html
E-Mail: hzhang@cs.uiowa.edu
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Unknown, Logic: Unknown, Size: Small

292. Senac: Web Page: http://www.can.nl/SystemsOverview/General/SENAC/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Unknown

293. SIMATH: Web Page: http://emmy.math.uni-sb.de/~simath/
E-Mail: simath@math.uni-sb.de
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small

294. Specware: Web Page: http://www.kestrel.edu/home/prototypes/specware.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Editor, Logic: Unknown, Size: Small

295. STeP: Web Page: http://www-step.stanford.edu/
E-Mail: step-comments@cs.stanford.edu
Architect: Zohar Manna, Henny Sipma
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small

296. SuchThat: Web Page: http://www.cs.rpi.edu/~schupp/suchthat/#verificat
E-Mail: schupp@cs.rpi.edu
Architect: Sibylle Schupp, Rüdiger Loos
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small

297. Sunrise: Web Page: http://www.cis.upenn.edu/~hol/sunrise/
E-Mail: homeier@saul.cis.upenn.edu
Architect: Peter Homeier
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

298. SVC: Web Page: http://verify.stanford.edu/SVC/
E-Mail: SVC@verify.stanford.edu
Architect: Jeremy Levitt
Language: C++
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small

299. VDM: Web Page: http://www.csr.ncl.ac.uk/vdm/
E-Mail: John.Fitzgerald@ncl.ac.uk
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small

300. WebEQ: Web Page: http://www.dessci.com/en/
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Commercial

301. XPNet: Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/xpnet/0.html
E-Mail: Unknown
Architect: Jawahar Chirimar, Carl Gunter, Myra VanInwegen
Language: Unknown
Category: Proof Checker
Interaction: Editor, Logic: Unknown, Size: Small

302. Zenon: Web Page: http://focal.inria.fr/zenon/
E-Mail: damien.doligez@inria.fr
Architect: Damien Doligez
Language: Objective CAML
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small