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