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 implementation language. There also are versions without samples and in black-on-white text. And there also are versions of this list grouped by alphabet, by category, 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.

## Assembly

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

## C

2. 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
3. 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
4. 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
5. 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
6. 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
7. 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
8. 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
9. 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
10. 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
11. 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
12. 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
13. 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
14. 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
15. 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
16. 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
17. 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
18. 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 19. 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 20. 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 21. 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 22. 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 23. 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 24. 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 25. 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 26. 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 27. 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 28. 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 29. 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 30. 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 31. 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 32. 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 33. 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 34. 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 35. 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 36. 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 37. 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 38. 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 39. 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 40. 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 41. 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 42. 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 43. 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 44. 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 45. 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 46. 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 47. 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 48. 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 49. 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 50. 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 51. 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 52. 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 53. 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 54. Yacas Web Page: http://yacas.sourceforge.net/ E-Mail: Unknown Architect: Ayal Pinkus Language: C++ Category: Computer Algebra Interaction: Dialog, Logic: None, Size: Small 55. 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 ## Clean 56. 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 ## CLU 57. 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 58. 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 ## Esterel 59. 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 ## Fortran 60. Scilab Web Page: http://www.scilab.org/ E-Mail: Unknown Architect: Unknown Language: C, Fortran Category: Computer Algebra Interaction: Dialog, Logic: None, Size: Large ## Haskell 61. 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 62. 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 63. 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 64. 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 65. 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 66. 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 67. 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 68. 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 69. 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 ## HGKM 70. 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 ## HTML 71. 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 72. 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 ## Java 73. 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 74. 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 75. 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 76. 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 77. 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 78. 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 79. 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 80. 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 81. 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 82. 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 83. 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 84. 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 85. WebEQ Web Page: http://www.dessci.com/en/ E-Mail: Unknown Architect: Unknown Language: Java Category: Authoring Interaction: Editor, Logic: Unknown, Size: Commercial ## Lisp 86. 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 87. 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 88. 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 89. 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 90. 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 91. 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 92. 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 93. 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 94. 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 95. 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 96. 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 97. 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 98. 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 99. 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 100. 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 101. 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 102. 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 103. 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 104. 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 105. 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 106. 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 107. 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 108. 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 109. 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 110. 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 111. 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 112. 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 113. 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 114. 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 115. 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 116. 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 117. 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 118. 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 119. 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 120. 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 121. 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 122. 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 123. 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 124. 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 125. 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 126. 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 ## Maple 127. 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 ## Mathematica 128. 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 129. 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 130. 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 ## Maude 131. 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 ## ML 132. 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 133. 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 134. 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 135. 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 136. 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 137. 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 138. 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 139. 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 140. 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 141. 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 142. 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 143. 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 144. 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 145. 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 146. 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 147. 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 148. 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 149. 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 150. 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 151. 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 152. 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 153. 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 154. 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 155. 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 156. 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 157. 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 158. 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 159. 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 160. 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 161. 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 162. 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 ## Modula 163. 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 ## Oz 164. 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 ## Pascal 165. 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 166. 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 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. 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
169. 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

## Prolog

170. 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
171. 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
172. 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
173. 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
174. 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
175. 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
176. 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
177. 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
178. 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
179. 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
180. 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
181. 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
182. 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
183. 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
184. 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

## Python

185. 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
186. 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
187. 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

## SGML

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. 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
190. 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
191. 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
192. 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
193. 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

## Tcl

194. 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
195. 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
196. 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

## XSL

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

## Unknown

198. 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
199. 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
200. 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
201. 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
202. 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
203. 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
204. 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
205. 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
206. 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
207. 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
208. 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
209. 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
210. 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
211. 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
212. 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
213. 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
214. 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
215. 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
216. Discount
E-Mail: denzinge@informatik.uni-kl.de
Architect: Jörg Denzinger
Language: Unknown
Category: Theorem Prover
Interaction: Script, Logic: Unknown, Size: Small
217. 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
218. DReaM
Web Page: http://dream.inf.ed.ac.uk/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown
219. 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
220. EPGY
Web Page: http://epgy.stanford.edu/TPE/
Architect: Rick Sommer, Pat Suppes
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Classical, Size: Small
221. Equplus
Web Page: http://equplus.net/
E-Mail: Unknown
Architect: Maria Chernenko
Language: Unknown
Category: Information
Interaction: Corpus, Logic: None, Size: Small
E-Mail: lav@unicyb.kiev.ua
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small
223. 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
224. Expressionist
Web Page: http://www.livemath.com/matheq/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
225. 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
226. 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
227. 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
228. 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
229. 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
230. 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
231. 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
232. 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
233. 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
234. 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
235. 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
236. 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
237. 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
238. 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
239. 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
240. 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
241. 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
242. 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
243. LiveMath
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
244. 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
245. 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
246. LogicCoach 9
E-Mail: n.pole@csuohio.edu
Architect: Nelson Pole
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small
247. 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
248. LogicWorks
Web Page: http://www.bgsu.edu/pdc/logicwo.html
E-Mail: lechar@bgnet.bgsu.edu
Language: Unknown
Category: Logic Education
Interaction: Dialog, Logic: Classical, Size: Commercial
249. 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
250. 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
251. 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
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
253. 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
254. 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
255. 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
E-Mail: Mark.Widholm@UNH.edu
Architect: Mark Widholm
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
257. MathScript
Web Page: http://www.mathscript.pair.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
258. 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
259. MathView
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
260. 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
261. 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
262. 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
263. 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
264. 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
265. MINSE
Web Page: http://lfw.org/math/
E-Mail: Unknown
Architect: Ka-Ping Yee
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
266. 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
267. 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
268. 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
269. 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
270. 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
271. 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
272. 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
273. 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
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
275. 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
276. 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
277. Purr
E-Mail: cm@eecs.berkeley.edu
Architect: Christoph Meyer
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
278. 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
279. 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
280. 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
281. 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
282. 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
283. 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
284. 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
285. 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
286. 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
287. 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
288. 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
289. 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
290. 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
291. STeP
Web Page: http://www-step.stanford.edu/
Architect: Zohar Manna, Henny Sipma
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small
292. 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
293. 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
294. 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
295. 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
296. 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
297. 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
298. 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
299. 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
300. 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
301. 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
302. 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