Digital Math by Language with Samples

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";

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: 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

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/
E-Mail: epgy-admin@epgy.stanford.edu
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

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

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: 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

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
Architect: Rob Brady
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

252. Mathcad: Web Page: http://www.mathcad.com/mathcad/
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

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

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

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

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: 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

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/
E-Mail: step-comments@cs.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