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 category. There also are versions without samples and in black-on-white text. And there also are versions of this list grouped by alphabet, by implementation language, by most common interaction mode, by the logic that is supported, 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.




Authoring


1. 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
2. Expressionist
Web Page: http://www.livemath.com/matheq/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
3. 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
4. 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
5. 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
6. 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
7. MathScript
Web Page: http://www.mathscript.pair.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
8. 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
9. 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
10. 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
11. TeX: LaTeX
\[(-1)^{r(\A)}\mu (\A)t^{r(\A)}.\]
The conclusion
follows by comparing coefficients of the leading
terms on both sides of the equation in
Corollary~\ref{tripleA}. If $H$ is a separator then
$r(\A') < r(\A)$ and there is no contribution
from $\pi (\A',t)$.
\end{proof}

The Poincar\'e polynomial of an arrangement
will appear repeatedly
in these notes. It will be shown to equal the
Poincar\'e polynomial
of the graded algebras which we are going to
associate with $\A$. It is also the Poincar\'e
polynomial of the complement $M(\A)$ for a
complex arrangement. Here we prove
that the Poincar\'e polynomial is the chamber
counting function for a real arrangement. The
complement $M(\A)$ is a disjoint union of chambers
\[M(\A) = \bigcup_{C \in \Cham(\A)} C.\]
The number
of chambers is determined by the Poincar\'e
polynomial as follows.

Web Page: http://www.tug.org/
E-Mail: Unknown
Architect: Donald Knuth, Leslie Lamport
Language: Pascal
Category: Authoring
Interaction: Script, Logic: None, Size: Large
12. WebEQ
Web Page: http://www.dessci.com/en/
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Commercial


Computer Algebra


13. 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
14. 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
15. 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
16. 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
17. 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
18. 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
19. 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
20. 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
21. 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
22. 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
23. 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
24. 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
25. 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
26. 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
27. 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
28. 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
29. 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
30. 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
31. 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
32. 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
33. 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
34. 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
35. 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
36. LiveMath
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
37. 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
38. 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
39. 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
40. 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
41. 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
42. 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
43. Mathcad
Web Page: http://www.mathcad.com/mathcad/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
44. 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
45. 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
46. 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
47. MathView
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
48. MathXpert
24. x^2 + 3xy + y^2 = 1, diff(y,t) = -2 | y= -1, x=0
25.  V = (4/3)pi r^3, diff(V,t) = -2| r=3
26. xy^2+4y - 44 = 0, diff(x,t) = 3 | y = 2
27. y = 4x^2 - 100, diff(y,t) = -6 | x = 1
28. 4x^2+y^2 = 25, diff(x,t) = 5 | x = 3/2, y = 4
29. 4x^2+y^2 = 25, diff(x,t) = 5| x = 3/2, y = -4
30. y - x^2+4x = -10, diff(y,t) = 3 | x = -2
31. x^2+xy+y = 16, diff(y,t) = 5 | x = 4
32. u^2 = x^2+(90)^2, diff(x,t) = 20| x = 30, u = -30 sqrt (10)
33. 48 S - 480 = S h, diff(h,t) = 32| S = 30, h = 32
34. y^2 = (30+x)^2 - (18)^2, diff(y,t) = 9| x = 6, y = 18 sqrt 3
35. y = 1 / (x^2 - 1), diff(y,t) = 1| x = -2
36. 2 y^3 - x^2+4x = -10, diff(y,t) = -3| x = -2, y = 1
37. A = 2 h sqrt (16+h^2), diff(A,t) = 2 | h = 3
38. A = x (600 - x) / 2, diff(A,t) = 4 | x = 200
39. x^2+y^3+z^4 = -3, diff(x,t) = -3, diff(z,t) = 4 | x = 2, y = -2, z = 1
40. xyz = 10, diff(x,t) = -2, diff(z,t) = 3| x = 2, y = -5, z = -1
41. V = 4 pi r^3 / 3, S = 4 pi r^2, diff(V,t) = 10 | r = 4
42. x = 20 tan theta, diff(x,t) = 4 | x = 15
43. y - x = sin y, diff(x,t) = 3 | y = pi / 2
44. h = 20 tan theta, diff(h,t) = 3 | theta = pi/6
45. L = 40 sec theta - 20 tan theta+ 30, diff(L,t) = -1 | theta = pi / 4
46. A = ( r  theta) / 2 - (sin theta) / 2, diff(r,t) = 1,  diff(A,t) = -1 | thet
a = pi/2, A = 1/4

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
49. 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
50. 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
51. 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
52. 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
53. 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
54. 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
55. 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
56. 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
57. 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
58. 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
59. 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
60. 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
61. 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
62. 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
63. Scilab
Web Page: http://www.scilab.org/
E-Mail: Unknown
Architect: Unknown
Language: C, Fortran
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
64. 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
65. 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
66. 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
67. 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
68. 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
69. 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
70. Yacas
Web Page: http://yacas.sourceforge.net/
E-Mail: Unknown
Architect: Ayal Pinkus
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small


First Order Prover


71. 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
72. 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
73. Bliksem
{ ! member( Z, compose( Xf, Xg)), equal( Z, ordered_pair( f29( Z, Xf, Xg), f30( 
Z, Xf, Xg)))}.
{ ! member( Z, compose( Xf, Xg)), member( ordered_pair( f29( Z, Xf, Xg), f31( Z,
 Xf, Xg)), Xf)}.
{ ! member( Z, compose( Xf, Xg)), member( ordered_pair( f31( Z, Xf, Xg), f30( Z,
 Xf, Xg)), Xg)}.
{ member( Z, compose( Xf, Xg)), ! little_set( Z), ! little_set( X), ! little_set
( Y), ! little_set( W), ! equal( Z, ordered_pair( X, Y)), ! member( ordered_pair
( X, W), Xf), ! member( ordered_pair( W, Y), Xg)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), closed( Xs1, Xf1)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), closed( Xs2, Xf2)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), maps( Xh, Xs1, Xs2)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! member( X, Xs1), ! member( Y, Xs1),
 equal( apply( Xh, apply_to_two_arguments( Xf1, X, Y)), apply_to_two_arguments( 
Xf2, apply( Xh, X), apply( Xh, Y)))}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), member( f32( Xh, Xs1, Xf1, Xs2, Xf2), Xs1)}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), member( f33( Xh, Xs1, Xf1, Xs2, Xf2), Xs1)}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), ! equal( apply( Xh, apply_to_two_arguments( Xf1, f32( 
Xh, Xs1, Xf1, Xs2, Xf2), f33( Xh, Xs1, Xf1, Xs2, Xf2))), apply_to_two_arguments(
 Xf2, apply( Xh, f32( Xh, Xs1, Xf1, Xs2, Xf2)), apply( Xh, f33( Xh, Xs1, Xf1, Xs
2, Xf2))))}.

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
74. 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
75. 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
76. 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
77. 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
78. 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
79. 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
80. 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
81. 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
82. Finder
 minister(x) = Doris, male(minister(x+1)) -> false.

 partner(Anita) = Horace.
 married(Anita) -> false.

 E!(partner(Boris)) -> false.
 minister(x+1) = Boris -> partner(minister(x)) = minister(x+2).

 male(minister(Football)).
 partner(minister(Football)) = wife.
 parent(Peter,wife).
 married(wife).

 married(minister(Fisheries)) -> false.

 minister(x) = Zita -> minister(opposite(x)) = Peter.

 minister(x+1) = Peter -> minister(x) = Vita, minister(x+2) = Vita.
}


setting {
 pre-test: 4
}

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
83. 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
84. FT
6.15 Ax(p(x)->~Ey(q(y)&r(x,y)))&Ax(t(x)->Ey(s(y)&r(x,y)))&Ax(p(x)->
                                   ~~t(x))&Ay(s(y)->q(y))->~Exp(x) [160]

  Comment: the designation "simple" is here pretty arbitrary: These are
just some short formulas, written down more or less at random, that
happen to be easily proved by the present algorithm.  Other short
formulas take "forever".


  7. Problematic

q(a1,a2,a1,a2) -> Ex1Ex2Ey1Ey2((p(x1)&p(x2) <-> p(y1)&p(y2)) & q(x1,x2,y1,y2)).
                                                                      [20]
q(a1,a2,a3,a1,a2,a3) -> Ex1Ex2Ex3Ey1Ey2Ey3((p(x1)&p(x2)&p(x3) <-> 
                          p(y1)&p(y2)&p(y3))&q(x1,x2,x3,y1,y2,y3)).
                                                                      [210]
q(a1,a2,a3,a4,a1,a2,a3,a4) -> Ex1Ex2Ex3Ex4Ey1Ey2Ey3Ey4(
 (p(x1)&p(x2)&p(x3)&p(x4) <-> p(y1)&p(y2)&p(y3)&p(y4))&
                          q(x1,x2,x3,x4,y1,y2,y3,y4)).                [16680]

q(a1,a2,a3,a4,a5,a1,a2,a3,a4,a5) -> Ex1Ex2Ex3Ex4Ex5Ey1Ey2Ey3Ey4Ey5(
(p(x1)&p(x2)&p(x3)&p(x4)&p(x5) <-> p(y1)&p(y2)&p(y3)&p(y4)&p(y5))&
                       q(x1,x2,x3,x4,x5,y1,y2,y3,y4,y5)).            [hopeless]

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
85. 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
86. 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
87. Kripke
++&bcaVo~b~ao~c~a;((a+b)&(a+c))>(a+(b&c))
++&ac&abV~ao~c~b;(a&(b+c))>((a&b)+(a&c))
+&+bcaoV~b~aV~c~a;((a&b)+(a&c))>(a&(b+c))
++&~c~b~aVoaboac;(ao(bVc))>((aob)V(aoc))
+&+~c~a+~b~aoaVbc;((aob)V(aoc))>(ao(bVc))
+&+~c~b~aoVabVac;(aV(boc))>((aVb)o(aVc))
++&~c~a&~b~aVaobc;((aVb)o(aVc))>(aV(boc))
++&o~b~ao~c~aaVbc;((a+b)V(a+c))>(a+(bVc))
++&~ao~c~bVabVac;(aV(b+c))>((aVb)+(aVc))
+o&~c~a&~b~aV+bca;((aVb)+(aVc))>(aV(b+c))
++~acVo&~c~bao&ab~c;((a>(bVc))&((a&b)>c))>(a>c)
++~aV~baVab;a>((~a&b)>(aVb))
++~aaV~aa;(a&~a)>(a>a)
+V~baV+~ab+aa;(~a&b)>((~a>a)V(a>b))
++~abVV~b~aa;(a&~a&b)>(a>b)
++~aV~baV+~aba;a>((~a&b)>(aV(a>b)))
+V~b~aV+~ab+aa;(a&b)>((~a>a)V(a>b))
+~aV+V~aab+aa;a>((~a>a)V((a&~a)>b))
VV++~aabao~ba;aV~(a>b)V(~a>(a>b))
+&+~bc+~aco~cVab;(aVb)>c>((a>c)&(b>c))
+&aVbc&~cV~b~a;((a&b)Vc)>(a&(bVc))
++~aVo~bao&~d~caV&bd&bc;((a>b)&(a>(cVd)))>(a>((b&c)V(b&d)))
+++~acVo&~c~bao~aaVo&ab~co~cc;((a>(bVc))&(a>a))>((((a&b)>c)&(c>c))>(a>c))
V+~ba+~ab;(a>b)V(b>a)

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
88. 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
89. 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
90. 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
91. Mace
% The numbers in comments are McCarthy's axiom numbers.
%

formula_list(usable).  % (formulas with explicit quantification)

% List the squares that are not allowed to be covered.

all x all y (G5(x,y) <-> (x=0 & y=0) | (x=7 & y=7)). % 11, 12

% Some test cases that are satisfiable:
%
% all x all y (G5(x,y) <-> (x=1 & y=1) | (x=1 & y=2) |
%                          (x=2 & y=2) | (x=3 & y=2) ).
%
% all x all y (G5(x,y) <-> (x=0 & y=1) | (x=7 & y=7)).
%
% all x all y -G5(x,y).   % complete board -- 12988816 models

end_of_list.

list(usable).  % clauses (symbols [u-z]+ are variables).

% Dominoes don't stick out.


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
92. 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
93. 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
94. Otter
% P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))).  %  axiom F2.
% P(i(i(x,i(y,z)),i(y,i(x,z)))).  %  axiom F3.
% P(i(i(x,y),i(n(y),n(x)))).  %  axiom F4.
% P(i(n(n(x)),x)).  %  axiom F5.
% P(i(x,n(n(x)))).  %  axiom f6.
end_of_list.
  
list(passive).
-P(i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s))) | $ANS(neg_th_04).
-P(i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r))))) | $ANS(neg_th_05).
-P(i(i(p,q),i(i(i(p,r),s),i(i(q,r),s)))) | $ANS(neg_th_06).
-P(i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s))))) | $ANS(neg_th_07).
-P(i(i(q,r),i(i(p,q),i(i(r,s),i(p,s))))) | $ANS(neg_th_08).
-P(i(i(i(n(p),q),r),i(p,r))) | $ANS(neg_th_09).
-P(i(p,i(i(i(n(p),p),p),i(i(q,p),p)))) | $ANS(neg_th_10).
-P(i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p))) | $ANS(neg_th_11).
-P(i(t,i(i(n(p),p),p))) | $ANS(neg_th_12).
-P(i(i(n(p),q),i(t,i(i(q,p),p)))) | $ANS(neg_th_13).
-P(i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r))) | $ANS(neg_th_14).
-P(i(i(n(p),q),i(i(q,p),p))) | $ANS(neg_th_15).
-P(i(p,p)) | $ANS(neg_th_16).
-P(i(p,i(i(q,p),p))) | $ANS(neg_th_17).
-P(i(q,i(p,q))) | $ANS(neg_th_18).
-P(i(i(i(p,q),r),i(q,r))) | $ANS(neg_th_19).

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
95. 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
96. 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
97. 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
98. 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
99. 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
100. 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
101. 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
102. 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
103. 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
104. 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
105. 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
106. 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
107. Smiley
{ ! member( Z, compose( Xf, Xg)), equal( Z, ordered_pair( f29( Z, Xf, Xg), f30( 
Z, Xf, Xg)))}.
{ ! member( Z, compose( Xf, Xg)), member( ordered_pair( f29( Z, Xf, Xg), f31( Z,
 Xf, Xg)), Xf)}.
{ ! member( Z, compose( Xf, Xg)), member( ordered_pair( f31( Z, Xf, Xg), f30( Z,
 Xf, Xg)), Xg)}.
{ member( Z, compose( Xf, Xg)), ! little_set( Z), ! little_set( X), ! little_set
( Y), ! little_set( W), ! equal( Z, ordered_pair( X, Y)), ! member( ordered_pair
( X, W), Xf), ! member( ordered_pair( W, Y), Xg)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), closed( Xs1, Xf1)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), closed( Xs2, Xf2)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), maps( Xh, Xs1, Xs2)}.
{ ! homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! member( X, Xs1), ! member( Y, Xs1),
 equal( apply( Xh, apply_to_two_arguments( Xf1, X, Y)), apply_to_two_arguments( 
Xf2, apply( Xh, X), apply( Xh, Y)))}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), member( f32( Xh, Xs1, Xf1, Xs2, Xf2), Xs1)}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), member( f33( Xh, Xs1, Xf1, Xs2, Xf2), Xs1)}.
{ homomorphism( Xh, Xs1, Xf1, Xs2, Xf2), ! closed( Xs1, Xf1), ! closed( Xs2, Xf2
), ! maps( Xh, Xs1, Xs2), ! equal( apply( Xh, apply_to_two_arguments( Xf1, f32( 
Xh, Xs1, Xf1, Xs2, Xf2), f33( Xh, Xs1, Xf1, Xs2, Xf2))), apply_to_two_arguments(
 Xf2, apply( Xh, f32( Xh, Xs1, Xf1, Xs2, Xf2)), apply( Xh, f33( Xh, Xs1, Xf1, Xs
2, Xf2))))}.

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
108. 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
109. 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
110. 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
111. 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
112. 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
113. 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
114. 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


Information


115. 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
116. 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
117. Equplus
Web Page: http://equplus.net/
E-Mail: Unknown
Architect: Maria Chernenko
Language: Unknown
Category: Information
Interaction: Corpus, Logic: None, Size: Small
118. 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
119. 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
120. 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
121. 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
122. 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
123. 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
124. 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
125. 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
126. 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


Logic Education


127. 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
128. 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
129. 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
130. 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
131. 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
132. 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
133. 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
134. 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
135. 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
136. 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
137. 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
138. 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
139. 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
140. 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
141. 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
142. 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
143. 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


Proof Checker


144. Automath: Aut
%set etared
th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
%reset etared
-imp
b@ec:=[x:a]not(<x>b):'prop'
[n:not(a)]
eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
b@[a1:and(a,b)]
ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b
a@[ksi:'type']
+ite
[x1:ksi][y1:ksi]
is:=is"l.e"(ksi,x1,y1):'prop'
-ite
[x:[t:a]ksi][y:[t:not(a)]ksi][i:[t:a][u:a]is".ite"(<t>x,<u>x)][j:[t:not(a)][u:no
t(a)]is".ite"(<t>y,<u>y)]
+*ite
j@[z:ksi]
prop1:=and(imp(a,[t:a]is(z,<t>x)),imp(not(a),[t:not(a)]is(z,<t>y))):'prop'
j@[a1:a][x1:ksi][y1:ksi][px1:prop1(x1)][py1:prop1(y1)]
t1:=ande1"l"(imp(a,[t:a]is(x1,<t>x)),imp(not(a),[t:not(a)]is(x1,<t>y)),px1):imp(
a,[t:a]is(x1,<t>x))
t2:=mp(a,[t:a]is(x1,<t>x),a1,t1):is(x1,<a1>x)
t3:=t2(y1,x1,py1,px1):is(y1,<a1>x)

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
145. 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
146. 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
147. 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
148. 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
149. 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
150. 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
151. 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
152. 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
153. 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
154. FLiP
[(Text('~Ax.P(x) |- Ex.~P(x)'), comment),
    (Not(A(x, P(x))), given),
    (Not(E(x, Not(P(x)))), assume),
    (New(x), new),
    (Not(P(x)), assume),
    (E(x, Not(P(x))), Ei, 4),
    (F, contra, 5,2),
    (Not(Not(P(x))), raa, 4,6),
    (P(x), ne, 7),
    (A(x, P(x)), Ai, 3,8),
    (F, contra, 9,1),
    (Not(Not(E(x, Not(P(x))))), raa, 2,10),
    (E(x, Not(P(x))), ne, 11)]

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
155. 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
156. Half: C-Half
                 app(k:Nat,f:(i:NN k)->QxQ,
                     g:(i:NN k)->IH ($Cons (xinI x (f i)) w2))=
                   case k of {
                    $z -> $Nil,
                    $s n -> th_finS.append 
                            (g ($Inr $True)).fst 
                            (app n (\i->f ($Inl i)) (\i->g ($Inl i)))}
                   :list S,
                 applem1(k:Nat,f:(i:NN k)->QxQ,
                         g:(i:NN k)->IH ($Cons (xinI x (f i)) w2))=
                   case k of {
                    $z -> $True,
                    $s n -> th_subsS.appfinsubset 
                            (g ($Inr $True)).fst 
                            (app n (\i->f ($Inl i)) (\i->g ($Inl i))) U 
                            (g ($Inr $True)).snd.fst 
                            (applem1 n (\i->f ($Inl i)) (\i->g ($Inl i)))}
                   :th_subsS.finsubset (app k f g) U,
                 applem2(k:Nat,f:(i:NN k)->QxQ,
                         g:(i:NN k)->IH ($Cons (xinI x (f i)) w2))=
                   case k of {
                    $z -> \i->
                      case i of {},
                       $s n -> \i->

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
157. 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
158. 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
159. 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
160. 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
161. 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
162. Ivy
(41 (instantiate 40 ((v64 . v0)(v65 . v1))) (or (not (P (-> v0 v1))) (P (-> (-> 
(- v0) v0) v1))) NIL)
(42 (instantiate 41 ((v0 . (-> v64 v65))(v1 . (-> (-> (- v64) v64) v65)))) (or (
not (P (-> (-> v64 v65) (-> (-> (- v64) v64) v65)))) (P (-> (-> (- (-> v64 v65))
 (-> v64 v65)) (-> (-> (- v64) v64) v65)))) NIL)
(43 (instantiate 21 ((v0 . v64)(v1 . v65))) (P (-> (-> v64 v65) (-> (-> (- v64) 
v64) v65))) NIL)
(44 (resolve 42 (1) 43 ()) (P (-> (-> (- (-> v64 v65)) (-> v64 v65)) (-> (-> (- 
v64) v64) v65))) NIL)
(45 (instantiate 44 ((v64 . v0)(v65 . v1))) (P (-> (-> (- (-> v0 v1)) (-> v0 v1)
) (-> (-> (- v0) v0) v1))) (21))
(46 (instantiate 1 ((v0 . (-> (-> (-> v64 v65) (-> v66 v65)) v67))(v1 . (-> (-> 
v66 v64) v67)))) (or (not (P (-> (-> (-> (-> v64 v65) (-> v66 v65)) v67) (-> (->
 v66 v64) v67)))) (or (not (P (-> (-> (-> v64 v65) (-> v66 v65)) v67))) (P (-> (
-> v66 v64) v67)))) NIL)
(47 (instantiate 13 ((v0 . v64)(v1 . v65)(v2 . v66)(v3 . v67))) (P (-> (-> (-> (
-> v64 v65) (-> v66 v65)) v67) (-> (-> v66 v64) v67))) NIL)
(48 (resolve 46 (1) 47 ()) (or (not (P (-> (-> (-> v64 v65) (-> v66 v65)) v67)))
 (P (-> (-> v66 v64) v67))) NIL)
(49 (instantiate 48 ((v64 . v0)(v65 . v1)(v66 . v2)(v67 . v3))) (or (not (P (-> 
(-> (-> v0 v1) (-> v2 v1)) v3))) (P (-> (-> v2 v0) v3))) NIL)
(50 (instantiate 49 ((v0 . (- v64))(v1 . v65)(v3 . (-> v64 (-> v2 v65))))) (or (
not (P (-> (-> (-> (- v64) v65) (-> v2 v65)) (-> v64 (-> v2 v65))))) (P (-> (-> 
v2 (- v64)) (-> v64 (-> v2 v65))))) NIL)

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
163. 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
164. 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
165. 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
166. Metamath
      $([5-Aug-93]$)
  $}

  ${
    mpii.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
    mpii.2 $e |- ch $.
    $( A doubly nested modus ponens inference. $)
    mpii   $p |- ( ph -> ( ps -> th ) ) $=
      ( wi com23 mpi ) ACBDGABCDEHFI $.
      $([31-Dec-93]$)
  $}

  ${
    mpd.1 $e |- ( ph -> ( ps -> ch ) ) $.
    mpd.2 $e |- ( ph -> ps ) $.
    $( A modus ponens deduction. $)
    mpd   $p |- ( ph -> ch ) $=
      ( wi a2i ax-mp ) ABFACFABCDGEH $.
      $([5-Aug-93]$)
  $}

  ${
    mpcom.1 $e |- ( ph -> ( ps -> ch ) ) $.
    mpcom.2 $e |- ( ps -> ph ) $.

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
167. Mizar
      c2.x is Element of Image c1 by a3,STRUCT_0:def 2; then
      ex a being Element of L st c1.a = c2.x by YELLOW_2:12; then
      x ˇ c2.x & c1.(c2.x) = c2.x by Th6,YELLOW_2:20;
     hence c1.x ˇ c2.x by WAYBEL_1:def 2;
    end;
   hence thesis by YELLOW_2:10;
  end;

begin :: The lattice of closure systems

definition
 let L be RelStr;
 func Sub L -> strict non empty RelStr means:
Def3:
  (for x being set holds x is Element of it iff x is strict SubRelStr of L) &
  for a,b being Element of it holds a ˇ b iff
   ex R being RelStr st b = R & a is SubRelStr of R;
 existence
  proof
   set X = {RelStr«A,B» where A is Subset of the carrier of L,
                B is Relation of A,A: B c= the InternalRel of L};
   consider a being Subset of the carrier of L;
    the carrier of subrelstr a = a &
    the InternalRel of subrelstr a c= the InternalRel of L

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
168. 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
169. 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
170. 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
171. 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
172. 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
173. 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
174. 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
175. 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
176. 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
177. 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
178. TinkerType
           \Gamma \COMMA @X@ [[@<:T@]] \COMMA @x:T_11@ \p @t_2@ \IN @T_2@
         }{
           \Gamma \p @let {X@ @,x}=t_1 in t_2@ \IN @T_2@
         }#}
  }
}

datatypes {
  core {
    type {
      refine tysome {#TySome of string * [[ty *]] ty#}
    }
  }
}

parsing {
  atype {
    refine tysome
      {#LCURLY SOME UCID [[OType]] COMMA Type RCURLY
          { fun ctx ->
              let ctx1 = addname ctx $3.v in
              TySome($3.v, [[$4 ctx,]] [[$6]] ctx1) }#}
    }
}

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
179. Tutch
  [ x' : nat, !y:nat. !z:nat. x' = y => y = z => x' = z;  % ind hyp (x)
    [ y : nat;
      [ z : nat;
        [ s(x') = 0;
          [ 0 = z;
     s(x') = z ];                      % eqEs0
          0 = z => s(x') = z ];
        s(x') = 0 => 0 = z => s(x') = z ];
      !z:nat. s(x') = 0 => 0 = z => s(x') = z;   % case (y = 0)
      [ y' : nat, !z:nat. s(x') = y' => y' = z => s(x') = z;
        [ z : nat;
          [ s(x') = s(y');
     [ s(y') = 0;
       s(x') = 0 ];                    % eqEs0
            s(y') = 0 => s(x') = 0 ];
          s(x') = s(y') => s(y') = 0 => s(x') = 0;     % case (z = 0)         

          [ z' : nat, s(x') = s(y') => s(y') = z' => s(x') = z';
            [ s(x') = s(y');
              [ s(y') = s(z');
                x' = y';                      % eqEss
                y' = z';                      % eqEss
                !z:nat. x' = y' => y' = z => x' = z;
                x' = y' => y' = z' => x' = z';

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
180. Twelf
      equ_assoc
      (equ_trans
         (equ_cong_* equ_ref equ_commute)
         (equ_cong_* 
     equ_ref
     Qd)))))
    <- flatten-n_sound F1 Q1
    <- flatten-n_sound F2 Q2
    <- equ_dist Qd.

fns_-1   : flatten-n_sound (fn_-1 F)
     (equ_trans
        Q
        (equ_cong_*
    equ_ref
    (equ_trans
       equ_ident
       (equ_trans
   (equ_cong_* equ_inverse equ_ref)
   (equ_trans
      equ_assoc
      (equ_trans
         (equ_cong_*
     equ_ref

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
181. 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


Representation


182. 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
183. 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
184. 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
185. DReaM
Web Page: http://dream.inf.ed.ac.uk/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown
186. 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
187. HDM
\begin{verbatim}
(defn number-field (X)
  (field X)
  (finite-extension X Q))
\end{verbatim}

\section{ProperSubset}

 Let $S$ be a set and let $X \subset S$ be a subset. We say $X$ is a
 {\em proper subset} of $S$ if $X \neq S$.

\begin{verbatim}
(defn proper-subset (X S)
  (set S)
  (subset X S)
  (neq X S))
\end{verbatim}

\section{DigitalSearchTree} \label{DigitalSearchTree-section}

 A \emph{digital search tree} is a tree which stores strings
 internally so that there is no need for extra leaf nodes to store the
 strings.


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
188. 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
189. 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
190. 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
191. 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
192. 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
193. 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
194. 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
195. 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
196. MINSE
Web Page: http://lfw.org/math/
E-Mail: Unknown
Architect: Ka-Ping Yee
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
197. 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
198. 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
199. 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
200. OpenMath
        </Description>
        <FunctorClass> Unary, Function </FunctorClass>
        <CDAttributes>
            Error( "logarithm has a singularity at 0" )
        </CDAttributes>
        <Signature> Intersect(real,positive) -> real </Signature>
        <Signature> symbolic -> symbolic </Signature>
        <CMP> ln(1) = 0 </CMP>
        <CMP> ln(exp(x)) = x, "for real x" </CMP>
        <CMP> exp(ln(x)) = x, always </CMP>
    </CDDefinition>

    <CDDefinition>
        <Name> sin </Name>
        <Description> The circular trigonometric function sine
            <Reference> M. Abramowitz and I. Stegun, Handbook of
                Mathematical Functions, [4.3]
            </Reference>
        </Description>
        <FunctorClass> Unary, Function </FunctorClass>
        <Signature> real -> real </Signature>
        <Signature> symbolic -> symbolic </Signature>
        <CMP> sin(0) = 0 </CMP>
        <CMP> sin(integer*Pi) = 0 </CMP>

Web Page: http://www.openmath.org/
E-Mail: Unknown
Architect: Gaston Gonnet
Language: SGML
Category: Representation
Interaction: Interface, Logic: None, Size: Small
201. 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
202. TPTP
    [++c3_2(U,a1762),
     ++ssSkP8(U)]).

input_clause(clause155,conjecture,
    [++c7_2(a1756,a1757),
     ++ssSkC43]).

input_clause(clause156,conjecture,
    [++c4_2(U,a1754),
     ++ssSkP7(U)]).

input_clause(clause157,conjecture,
    [++c8_2(U,a1754),
     ++ssSkP7(U)]).

input_clause(clause158,conjecture,
    [++c2_2(U,a1754),
     ++ssSkP7(U)]).

input_clause(clause159,conjecture,
    [++c2_2(a1743,a1744),
     ++ssSkC39]).

input_clause(clause160,conjecture,

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
203. 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


Specification Environment


204. 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
205. 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
206. 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
207. 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
208. 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
209. 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
210. 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
211. 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
212. 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
213. 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
214. 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
215. 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
216. 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
217. 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
218. 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
219. 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
220. 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
221. 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
222. 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
223. 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
224. 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
225. 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
226. 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
227. 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
228. 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
229. 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
230. 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
231. 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
232. 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
233. 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


Tactic Prover


234. 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
235. Coq
Save.
(* End of proof of lem_rel_Comp_rel_sig                                    *)

(***************************************************************************)
(* Reunion de relations                                                    *)
(***************************************************************************)
Definition rel_union :=
  [r1,a1,b1:E][r2,a2,b2:E][rRel1:(rel_sig r1 a1 b1)][rRel2:(rel_sig r2 a2 b2)]
    (union r1 r2)
.

Lemma lem_rel_union_rel_sig :
  (r1,a1,b1:E)(r2,a2,b2:E)(rRel1:(rel_sig r1 a1 b1))(rRel2:(rel_sig r2 a2 b2))
    (rel_sig 
      (rel_union r1 a1 b1 r2 a2 b2 rRel1 rRel2)
      (union a1 a2) (union b1 b2)
    )
.
(* Proof of lem_rel_union_rel_sig                                          *)
(Unfold rel_union;Unfold rel_sig;Unfold inc;Intros).
(Elim (lem_union_propertie r1 r2 v0);Intros;Generalize (H0 H);Clear H H0 H1;Intr
os).
(Elim (lem_cartesian_propertie (union a1 a2) (union b1 b2) v0);Intros;Apply H1;C

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
236. 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
237. 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
238. 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
239. 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
240. 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
241. 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
242. HOL: HOL Light
let REAL_SUB_REFL = prove(
  `!x. x - x = &0`,
  GEN_TAC THEN REWRITE_TAC[real_sub; REAL_ADD_RINV]);;

let REAL_SUB_0 = prove(
  `!x y. (x - y = &0) = (x = y)`,
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [DISCH_THEN(MP_TAC o C AP_THM `y:real` o AP_TERM `(+)`) THEN
    REWRITE_TAC[REAL_SUB_ADD; REAL_ADD_LID];
    DISCH_THEN SUBST1_TAC THEN MATCH_ACCEPT_TAC REAL_SUB_REFL]);;

let REAL_LE_DOUBLE = prove(
  `!x. &0 <= x + x = &0 <= x`,
  GEN_TAC THEN EQ_TAC THENL
   [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN
    DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2 o W CONJ);
    DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_ADD2 o W CONJ)] THEN
  REWRITE_TAC[REAL_ADD_LID]);;

let REAL_LE_NEGL = prove(
  `!x. (--x <= x) = (&0 <= x)`,
  GEN_TAC THEN SUBST1_TAC (SYM(SPECL [`x:real`; `--x`; `x:real`] REAL_LE_LADD))
  THEN REWRITE_TAC[REAL_ADD_RINV; REAL_LE_DOUBLE]);;

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
243. HOL: HOL98
   REPEAT GEN_TAC
    THEN REWRITE_TAC[NEXT]
    THEN STRIP_TAC
    THEN ASM_CASES_TAC (--`(x2:num) = x3`--)
    THEN ASM_CASES_TAC (--`x2 < x3`--)
    THEN ASM_REWRITE_TAC[]
    THEN IMP_RES_TAC LESS_CASES_IMP
    THEN RES_TAC);

val next_SUC =
 DISCH_ALL
  (REWRITE_RULE
   [ADD_CLAUSES] 
   (SUBS [ASSUME (--`d = 0`--)]
         (ASSUME (--`(done:num->bool) (SUC x + d)`--))));

val NEXT_LEMMA2 =
 store_thm
  ("NEXT_LEMMA2",
   --`!x d done.
      (NEXT (x,(SUC x)+d) done /\ ~(done(SUC x))) ==> ~(d = 0)`--,
   REWRITE_TAC[NEXT]
    THEN REPEAT STRIP_TAC
    THEN IMP_RES_TAC next_SUC

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
244. 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
245. 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
246. 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
247. 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
248. Lego
Goal iclBase : IntersectionClosed Fbase;
Refine iclAnd;Refine iclSwap;Refine iclConscl;
Save iclBase;

[PermBase = intersectionRel Fbase];
[swapBase = fst (intFhasF Fbase iclBase):swap PermBase];
[consclBase = snd (intFhasF Fbase iclBase):consClosed PermBase];

[Perm = closure (equiv|(list A)) PermBase];

Goal equivPerm : equiv Perm;
Refine closureI;Refine iclEquiv;
Save equivPerm;

[reflPerm = fst equivPerm:refl Perm];
[symPerm = fst(snd equivPerm):sym Perm];
[transPerm = snd(snd equivPerm):trans Perm];

Goal SubRel (Eq|(list A)) Perm;
Intros;Qrepl hyp;Refine reflPerm;Try Immed;
Save reflPerm';

Goal swapPerm : swap Perm;

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
249. 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
250. 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
251. Minlog
;warshall-KERNEL-BASE-KERNEL-CASE-FALSE-CASE-FALSE: (rel j k -> F) -> (j=k -> F)
 -> ex x^.def x^ & (x^=eps -> all y.path rel 0 y j k -> F) & ((x^=eps -> F) -> p
ath rel 0 x^ j k & wf x^) from
;  rel  j  k

;warshall-KERNEL-BASE-KERNEL-CASE-FALSE-CASE-TRUE: rel j k -> (j=k -> F) -> ex x
^.def x^ & (x^=eps -> all y.path rel 0 y j k -> F) & ((x^=eps -> F) -> path rel 
0 x^ j k & wf x^) from
;  rel  j  k

;; Case rel j k
(assume 'hyp1 'hyp2)
(ex-intro (pt "con j(con k eps)"))
(split)
(split)
(ng)
(prop)
(ng)
(auto)
(assume 'hyp)
(drop 'hyp)
(split)
(ng)
(prop)

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
252. 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
253. 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
254. 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
255. Plastic
 [La_ : (f:(x:El A)El B)Pi_ ];

Claim ap_ : (A,B:Type) Pi_ A B -> A -> B;
Intros A B f x;
Refine E_Pi_ ? ? ([_:?]B); 
Refine f;
Intros fo;
Refine fo x;
ReturnAll;

Claim if_leq : (x,y:Nat)(T:Type)T -> T -> T;
Intros x y T leq not_leq;
Refine ap_ ? ? (ap_ ? ? ? x) y;

Refine La_;
Intros x1;
Refine E_Nat ([_:?]Pi_ Nat T) ?x_z ?x_s x1;
x_z Refine La_ ? ? ([_:?]leq);
Intros x1_ f_x1_;
Refine La_;
Intros y1;
Refine E_Nat ([_:?]T) ?y_z ?y_s y1;
y_z Refine not_leq;
Intros y1_ _;

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
256. 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
257. 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
258. Typelab
% Functions on Bool:

%defn fold__Bool := rec__Bool;
rec fold__Bool (T|Type,b__true,b__false:T,b:Bool):T :=
  case b of
    true => b__true
  | false => b__false
  end;

%defn if := fun (T|Type,b:Bool,b__true,b__false:T)
%             fold__Bool b__true b__false b;

rec if (T|Type,b:Bool,b__true,b__false:T) : T :=
    case b of
      true => b__true
    | false => b__false
    end;  

%defn \/ := fun (b:Bool) fold__Bool true b;
rec \/ (a,b:Bool) : Bool :=
    case a of
      true => true
    | false => case b of 

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
259. Yarrow
rewrite reverse_cons then rewrite reverse_nil
rewrite nil_concat
unfold singleton
rewrite cons_concat
rewrite nil_concat
refl
exit

def map := \A,B:*s. \f:A->B. primreclist (nil B) (
                                          \a:A. \bs:List B. (f a);bs) :
           @A,B:*s. (A->B) -> List A -> List B
implicit 2 map


prove map_nil : @A,B:*s. @f:A->B. map f (nil A) = nil B
intros
unfold map
rewrite primreclist_nil
refl
exit

prove map_cons : @A,B:*s. @f:A->B. @a:A. @as:List A. 
                 map f (a;as) = f a ; map f as
intros

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


Theorem Prover


260. 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
261. 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
262. 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
263. 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
264. 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
265. 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
266. 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
267. 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
268. 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
269. 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
270. Goedel
example[x271,"or[equal[first[x],x],
member[pair[first[x],second[x]],cart[V,V]]]",""]

example[x272,"or[equal[second[x],x],
member[pair[first[x],second[x]],cart[V,V]]]",""]

example[x273,"or[not[member[pair[x,y],cart[V,V]]],
equal[first[pair[x,y]],x]]",""]

example[x274,"or[not[member[pair[x,y],cart[V,V]]],
equal[second[pair[x,y]],y]]",""]

example[x275,"or[not[equal[pair[first[x],second[x]],x]],member[x,V]]",""]

example[x276,"or[not[equal[pair[first[x],second[x]],x]],
member[x,cart[V,V]]]",""]

example[x277,"or[not[equal[pair[x,y],pair[z,u]]],not[member[x,V]],
equal[x,z]]",""]

example[x278,"or[equal[first[pair[x,y]],pair[x,y]],member[x,V]]",""]

example[x279,"or[equal[second[pair[x,y]],pair[x,y]],member[x,V]]",""]

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
271. 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
272. 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
273. 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
274. 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
275. 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
276. IMPS
     (block
      (script-comment "`cut-with-single-formula' at (0)")
      (contrapose "with(p:prop,not(p));")
      (cut-with-single-formula "not(positive%prime(prod(2,k,lambda(j:zz,j))+1))"
)
      (move-to-sibling 1)
      (block
       (script-comment "`cut-with-single-formula' at (1)")
       (backchain "with(p:prop,forall(m:zz,p));")
       (block
 (script-comment "`backchain' at (0)")
 (weaken (0))
 unfold-defined-constants
 (cut-with-single-formula "k=0 or k=1 or 2<=k ")
 (move-to-sibling 1)
 simplify
 (block
  (script-comment "`cut-with-single-formula' at (0)")
  (antecedent-inference "with(p:prop,p or p or p);")
  simplify
  simplify
  (block
   (script-comment "`antecedent-inference' at (2)")
   simplify

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
277. 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
278. IPR
(def-theorem kelley-5-18
  (implies (and (a-nbhd-of-the-set u_ a_ x_)
  (closed-in a_ x_)
  (a-compact-subset-of a_ x_)
  (a-regular-top-space x_)
  (a-locally-compact-top-space x_))
    (for-some ((v))
      (and (closed-in v_ x_)
    (a-nbhd-of-the-set v_ a_ x_)
    (a-compact-subset-of v_ x_)
    (a-subset-of a_ v_)
    (a-subset-of v_ u_)
    (for-some ((f))
      (and (a-continuous-function-from-onto
     f _x (the-closed-unit-interval-top-space))
    (= (the-image-of f a_) (the-singleton (real-zero)))
    (= (the-image-of f (the-relative-complement x_ v_))
       (the-singleton (real-one)))))))))

(def-theorem kelley-p-147a
  (implies (and (a-locally-compact-top-space x_)
  (a-regular-top-space x_))
    (completely-regular x_)))


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
279. 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
280. 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
281. 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
282. Marcel
assign "?n_1" "(Nat:?m)+Nat:?n";
assign "?p_1" "?p";
up();ri "3pt66";ex();
rri "CRULE3";ex();
right();ri "($ASSERT2)**BOOLDEF";ex();
ri "EQUATION**1|-|1";ex();
up();ri "CZER";ex();
up();ex();
ri "REALSUBNATTYPE**ASRTCOND";ex();
left();rri "CID";ex();
right();initializecounter();

rri "LEQ_ADD";ex();   (* from web page,but I have to remove bool *)
ri "RIGHT@RIGHT@PLUSTYPE2";ex();
ri "RIGHT@LESS_OR_EQ";ex();
ri "($ORBOOL)** $LESS_OR_EQ";ex();
assign "?m_1" "?n";
assign "?n_1" "?m";
ri "RIGHT@RIGHT@PLUSCOMM";ex();
up();ri "CSYM** $CRULE1";ex();
rri "CID";ex();
right();initializecounter();
rri "LEQ_LESS_TRANS";ex(); 
assign "?m_1" "?n";

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
283. 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
284. 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
285. Nqthm
(PROVE-LEMMA REMAINDER-TIMES
             (REWRITE)
             (EQUAL (REMAINDER (TIMES Y X) Y) '0)
             ((ENABLE COMMUTATIVITY-OF-TIMES DIVIDES-TIMES)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE REMAINDER-TIMES)

(PROVE-LEMMA QUOTIENT-TIMES
             (REWRITE)
             (EQUAL (QUOTIENT (TIMES Y X) Y)
                    (IF (ZEROP Y) '0 (FIX X)))
             ((ENABLE TIMES-ZERO2 COMMUTATIVITY-OF-TIMES DIFFERENCE-PLUS1)
              (ENABLE-THEORY GROUND-ZERO)
              (DISABLE-THEORY T)))

(DISABLE QUOTIENT-TIMES)

(PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A)) (DIVIDES A W))
                      (EQUAL (TIMES C (QUOTIENT W A))

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
286. 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
287. 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
288. 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
289. 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
290. 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
291. 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
292. 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
293. PVS
  subset_emptyset: LEMMA subset?(emptyset, a)

  subset_fullset: LEMMA subset?(a, fullset)

  union_idempotent: LEMMA union(a, a) = a

  union_commutative: LEMMA union(a, b) = union(b, a)

  union_associative: LEMMA union(union(a, b), c) = union(a, union(b, c))

  union_empty: LEMMA union(a, emptyset) = a

  union_full: LEMMA union(a, fullset) = fullset

  union_subset1: LEMMA subset?(a, union(a, b))

  union_subset2: LEMMA subset?(a, b) IMPLIES union(a, b) = b

  union_upper_bound : LEMMA
    subset?(a, c) and subset?(b, c) IMPLIES subset?(union(a, b), c)
  
  union_difference: LEMMA union(a, b) = union(a, difference(b, a))

  union_diff_subset: LEMMA subset?(a, b) IMPLIES union(a, difference(b, a)) = b

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
294. 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
295. 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
296. 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
297. 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
298. 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
299. 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
300. 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
301. Watson
assign "?n_1" "(Nat:?m)+Nat:?n";
assign "?p_1" "?p";
up();ri "3pt66";ex();
rri "CRULE3";ex();
right();ri "($ASSERT2)**BOOLDEF";ex();
ri "EQUATION**1|-|1";ex();
up();ri "CZER";ex();
up();ex();
ri "REALSUBNATTYPE**ASRTCOND";ex();
left();rri "CID";ex();
right();initializecounter();

rri "LEQ_ADD";ex();   (* from web page,but I have to remove bool *)
ri "RIGHT@RIGHT@PLUSTYPE2";ex();
ri "RIGHT@LESS_OR_EQ";ex();
ri "($ORBOOL)** $LESS_OR_EQ";ex();
assign "?m_1" "?n";
assign "?n_1" "?m";
ri "RIGHT@RIGHT@PLUSCOMM";ex();
up();ri "CSYM** $CRULE1";ex();
rri "CID";ex();
right();initializecounter();
rri "LEQ_LESS_TRANS";ex(); 
assign "?m_1" "?n";

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
302. Weierstrass
% irrationality of e

goal # all(p:N,all(q:N, exists(C,((0<q)-> and((abs(e-p/q) >= C/q!),(0<C)))))).

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