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

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

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




Both


1. Akka
Web Page: http://turing.wins.uva.nl/~lhendrik/AkkaStart.html
E-Mail: lhendrik@wins.uva.nl
Architect: Lex Hendriks
Language: Tcl
Category: Logic Education
Interaction: Unknown, Logic: Both, Size: Small
2. CYP
Web Page: ftp://ftp-sop.inria.fr/lemme/cyp/index.html
E-Mail: thery@sophia.inria.fr
Architect: Laurent Théry
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Both, Size: Small
3. Fellowship
Web Page: http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/fellowship/
E-Mail: Unknown
Architect: Florent Kirchner, Claudio Sacerdoti Coen
Language: Objective CAML
Category: Tactic Prover
Interaction: Dialog, Logic: Both, Size: Small
4. FLiP
[(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
5. Gandalf
Web Page: http://www.cs.chalmers.se/~tammet/gandalf/
E-Mail: tammet@cs.chalmers.se
Architect: Tanel Tammet
Language: Scheme
Category: First Order Prover
Interaction: Script, Logic: Both, Size: Small
6. ICLE
Web Page: http://www.doc.ic.ac.uk/~md/
E-Mail: md@doc.ic.ac.uk
Architect: Mark Dawson
Language: Omega Prolog
Category: Proof Checker
Interaction: Editor, Logic: Both, Size: Small
7. Isabelle
Web Page: http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Mailing List: isabelle-users@cl.cam.ac.uk
Architect: Larry Paulson, e.a.
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Both, Size: Large
8. Isabelle: Isar
Web Page: http://isabelle.in.tum.de/Isar/
E-Mail: wenzelm@in.tum.de
Architect: Markus Wenzel
Language: Standard ML
Category: Tactic Prover
Interaction: Editor, Logic: Both, Size: Small
9. Jape
Web Page: http://users.comlab.ox.ac.uk/bernard.sufrin/jape.html
E-Mail: Unknown
Architect: Bernard Sufrin, Richard Bornat
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small
10. Logics Workbench, LWB
Web Page: http://www.lwb.unibe.ch/
E-Mail: lwb@iam.unibe.ch
Architect: Gerhard Jaeger
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small
11. MacLogic
Web Page: http://www-theory.dcs.st-and.ac.uk/~rd/logic/mac/
E-Mail: rd@dcs.st-and.ac.uk
Architect: Roy Dyckhoff
Language: MacProlog
Category: Logic Education
Interaction: Editor, Logic: Both, Size: Small
12. OBJ
Web Page: http://archive.comlab.ox.ac.uk/obj.html
E-Mail: Unknown
Architect: Joseph Goguen
Language: Common Lisp
Category: Specification Environment
Interaction: Interface, Logic: Both, Size: Large
13. Proof General
Web Page: http://proofgeneral.inf.ed.ac.uk/
E-Mail: proofgen@dcs.ed.ac.uk
Architect: Thomas Kleymann, e.a.
Language: Emacs Lisp
Category: Authoring
Interaction: Editor, Logic: Both, Size: Small
14. Theax
Web Page: http://markun.cs.shinshu-u.ac.jp/kiso/projects/mathematics/Theax-e/Math-e-tit.htm
E-Mail: ynakamur@cs.shinshu-u.ac.jp
Architect: Yatsuka Nakamura
Language: Pascal, C
Category: Proof Checker
Interaction: Batch, Logic: Both, Size: Small
15. TinkerType
           \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


Classical


16. 3TaP
Web Page: http://mathforum.org/library/view/17325.html
E-Mail: beckert@uni-koblenz.de
Architect: Reiner Haehnle, Bernhard Beckert
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
17. ACL2
Web Page: http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html
E-Mail: Unknown
Architect: J. Strother Moore, e.a.
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large
18. Alfie
Web Page: http://www.cs.chalmers.se/~sydow/alfie/index.html
E-Mail: Unknown
Architect: Björn von Sydow
Language: Haskell
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small
19. Analytica
Web Page: http://andrej.com/analytica/
E-Mail: Edmund.Clarke@cs.cmu.edu
Architect: Edmund Clarke, Xudong Zhao
Language: Mathematica
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
20. Automath: Aut
%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
21. Bertie3, Twootie
Web Page: http://www.ucc.uconn.edu/~wwwphil/software.html
E-Mail: aclark@uconnvm.uconn.edu
Architect: Austen Clark
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small
22. Bertrand
Web Page: http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html
E-Mail: herzberg@kagi.com
Architect: Larry Herzberg
Language: Unknown
Category: First Order Prover
Interaction: Editor, Logic: Classical, Size: Small
23. Bliksem
{ ! 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
24. Class
Web Page: http://class-int.narod.ru
E-Mail: urchick@mail.ru
Architect: Yuri Vtorushin, Oleg Okhotnikov
Language: C++
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small
25. CLIN
Web Page: http://www.cs.unc.edu/Research/mi/mi-provers.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
26. Cocktail
Web Page: http://www.win.tue.nl/~michaelf/cocktail.html
E-Mail: michaelf@win.tue.nl
Architect: Michael Franssen
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
27. Coq: Pcoq
Web Page: http://www-sop.inria.fr/lemme/pcoq/
E-Mail: bertot@paprika.inria.fr
Architect: Yves Bertot
Language: Java
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small
28. Darwin
Web Page: http://www.mpi-sb.mpg.de/~baumgart/DARWIN/
E-Mail: baumgart@mpi-sb.mpg.de
Architect: Alexander Fuchs
Language: Objective CAML
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
29. DCTP
Web Page: http://www4.in.tum.de/~stenzg/
E-Mail: stenzg@mpi-sb.mpg.de
Architect: Gernot Stenz
Language: Scheme
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
30. Declare
Web Page: http://research.microsoft.com/~dsyme/declare.aspx
E-Mail: dsyme@microsoft.com
Architect: Don Syme
Language: Objective CAML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
31. DITLU
Web Page: http://www.dcs.qmul.ac.uk/~uhmm/info/caar.html
E-Mail: aaa@cs.st-andrews.ac.uk
Architect: Andrew Adams
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: Classical, Size: Small
32. DN
Web Page: http://bailhache.humana.univ-nantes.fr/dnfn/deductioneng.html
E-Mail: patrice.bailhache@humana.univ-nantes.fr
Architect: Patrice Bailhache
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small
33. Doris
Web Page: http://www.coli.uni-saarland.de/~bos/atp/doris-info.html
E-Mail: bos@coli.uni-sb.de
Architect: Johan Bos
Language: Prolog
Category: Theorem Prover
Interaction: Batch, Logic: Classical, Size: Small
34. DOVE: Isabelle
Web Page: http://www.dsto.defence.gov.au/esrl/itd/dove
E-Mail: Tony.Cant@dsto.defence.gov.au
Architect: Tony Cant
Language: Tcl
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small
35. DReaM
Web Page: http://dream.inf.ed.ac.uk/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown
36. E
Web Page: http://www.eprover.org/
E-Mail: schulz@informatik.tu-muenchen.de
Architect: Stephan Schulz
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
37. EHDM
Web Page: http://www.csl.sri.com/users/rushby/
E-Mail: Unknown
Architect: John Rushby, Sam Owre
Language: Lucid Common Lisp
Category: Specification Environment
Interaction: Dialog, Logic: Classical, Size: Small
38. EPGY
Web Page: http://epgy.stanford.edu/TPE/
E-Mail: epgy-admin@epgy.stanford.edu
Architect: Rick Sommer, Pat Suppes
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Classical, Size: Small
39. EQP
Web Page: http://www-unix.mcs.anl.gov/AR/eqp/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
40. ERA
Web Page: http://www.eecs.ku.edu/faculty_staff/bio/faculty/andygill
E-Mail: Unknown
Architect: Andy Gill
Language: Haskell
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Small
41. EVES
Web Page: http://www.springerlink.com/content/p225421w45016110/
E-Mail: Unknown
Architect: Sentot Kromodimoeljo, Irwin Meisels, Mark Saaltink, Bill Pase, Dan Craigen
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Commercial
42. Expander2
Web Page: http://fldit-www.cs.uni-dortmund.de/~peter/
E-Mail: peter.padawitz@udo.edu
Architect: Peter Padawitz
Language: O'Haskell
Category: Theorem Prover
Interaction: Editor, Logic: Classical, Size: Small
43. FDPLL
Web Page: http://www.uni-koblenz.de/~peter/FDP/
E-Mail: peter@uni-koblenz.de
Architect: Peter Baumgartner
Language: Eclipse Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
44. Finder
 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
45. Fitch, Boole, Tarski's World, Grade Grinder
Web Page: http://www-csli.stanford.edu/LPL/
E-Mail: Unknown
Architect: John Barwise, John Etchemendy, Gerard Allwein, Dave Barker-Plummer, Albert Liu
Language: Java, C
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Commercial
46. Funmath
Web Page: http://www.funmath.be/
E-Mail: boute@intec.UGent.be
Architect: Raymond Boute
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Classical, Size: Small
47. Getfol
Web Page: http://www.cs.unitn.it/~getfol/startgwigb.html
E-Mail: Unknown
Architect: Fausto Giunchiglia
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
48. Ghilbert
Web Page: http://www.ghilbert.org/
E-Mail: raph@acm.org
Architect: Raph Levien
Language: Python
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small
49. Goedel
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
50. HLM
Web Page: http://hlm.sourceforge.net/
E-Mail: SebastianR@gmx.de
Architect: Sebastian Reichelt
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
51. HOL: HOL Light
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
52. 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
53. Hyperproof
Web Page: http://www-csli.stanford.edu/hp/index.html#Hyperproof
E-Mail: Unknown
Architect: Gerry Allwein, Mark Greaves, Mike Lenz
Language: C, Pascal, Assembly
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Large
54. ICS
Web Page: http://www.icansolve.com/
E-Mail: ruess@csl.sri.com
Architect: Jean-Christophe Filliâtre
Language: Objective CAML
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
55. IMPS
     (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
56. INKA
Web Page: http://www.dfki.de/vse/systems/inka/
E-Mail: Unknown
Architect: Dieter Hutter
Language: Lucid Common Lisp
Category: Theorem Prover
Interaction: Editor, Logic: Classical, Size: Small
57. Isabelle: TAS, IsaWin
Web Page: http://www.informatik.uni-bremen.de/~cxl/tas/home.html
E-Mail: cxl@informatik.uni-bremen.de
Architect: Christoph Lüth, Burkhart Wolff
Language: Standard ML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
58. Ivy
(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
59. Kimba
Web Page: http://www.ags.uni-sb.de/~konrad/kimba.html
E-Mail: konrad@ags.uni-sb.de
Architect: Karsten Konrad
Language: Oz
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
60. Larch: LP
Web Page: http://www.sds.lcs.mit.edu/spd/larch/LP/overview.html
E-Mail: Unknown
Architect: Stephen Garland, John Guttag
Language: CLU
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large
61. Larch: LSL
Web Page: http://www.sds.lcs.mit.edu/spd/larch/lsl.html
E-Mail: Unknown
Architect: Stephen Garland, John Guttag
Language: CLU
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Large
62. leanTAP
Web Page: http://i12www.ira.uka.de/leantap/
E-Mail: beckert@ira.uka.de
Architect: Bernhard Beckert, Joachim Posegga
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
63. Leo
Web Page: http://www.ags.uni-sb.de/~omega/www/leo.html
E-Mail: chris@ags.uni-sb.de
Architect: Christoph Benzmüller
Language: Common Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
64. LogicCoach 9
Web Page: http://academic.csuohio.edu/polen/
E-Mail: n.pole@csuohio.edu
Architect: Nelson Pole
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small
65. LogicWorks
Web Page: http://www.bgsu.edu/pdc/logicwo.html
E-Mail: lechar@bgnet.bgsu.edu
Architect: Rob Brady
Language: Unknown
Category: Logic Education
Interaction: Dialog, Logic: Classical, Size: Commercial
66. Mace
% 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
67. 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
68. MathScheme
Web Page: http://imps.mcmaster.ca/mathscheme/
E-Mail: wmfarmer@mcmaster.ca
Architect: William M. Farmer, Martin v. Mohrenschildt
Language: Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Classical, Size: Small
69. MathXpert
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
70. 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
71. METEOR
Web Page: http://www.cs.duke.edu/~ola/meteor.html
E-Mail: ola@cs.duke.edu
Architect: Owen Astrachan
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
72. Mizar
      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
73. Mural
Web Page: http://www.cis.rl.ac.uk/proj/mural.html
E-Mail: Unknown
Architect: Brian Ritchie
Language: Unknown
Category: Specification Environment
Interaction: Editor, Logic: Classical, Size: Small
74. Nqthm
(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
75. Nqthm: PC-Nqthm
Web Page: http://www.computationallogic.com/software/pc-nqthm/index.html
E-Mail: Unknown
Architect: Matt Kaufman
Language: Common Lisp
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Unknown
76. Omega
Web Page: http://www.ags.uni-sb.de/~omega/
E-Mail: kohlhase@ags.uni-sb.de
Architect: Michael Kohlhase
Language: Common Lisp, CLOS
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large
77. Ontic
Web Page: http://www-cgi.cs.cmu.edu./afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html
E-Mail: ontic-implementors@ai.mit.edu
Architect: David McAllester
Language: Common Lisp
Category: Proof Checker
Interaction: Dialog, Logic: Classical, Size: Small
78. OpenProof
Web Page: http://www-vil.cs.indiana.edu/hwc4.html
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Unknown
79. OSHL
Web Page: http://www.cs.unc.edu/~plaisted/
E-Mail: zhu@cs.unc.edu
Architect: Yunshan Zhu, David Plaisted
Language: ECLiPSe Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
80. Otter
% 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
81. Paradox
Web Page: http://www.cs.chalmers.se/~koen/paradox/
E-Mail: koen@cs.chalmers.se
Architect: Koen Claessen, Niklas Sörensson
Language: Haskell, C++
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
82. Peers
Web Page: http://www.cs.uiowa.edu/~bonacina/cd.html
E-Mail: bonacina@cs.uiowa.edu
Architect: Maria Paola Bonacina
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
83. ProCom
Web Page: ftp://www.koralle.imn.htwk-leipzig.de/pub/ProCom/procom.html
E-Mail: Unknown
Architect: Gerd Neugebauer
Language: ECLiPSe Prolog
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
84. ProofCheck
Web Page: http://www.proofcheck.org/
E-Mail: neveln@cs.widener.edu
Architect: Bob Neveln
Language: Python
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small
85. ProofPower
Web Page: http://www.lemma-one.com/ProofPower/index/
E-Mail: rda@lemma-one.com
Architect: Rob Arthan, Roger Bishop Jones
Language: Standard ML
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Large
86. Proof Tutor
Web Page: http://hss.cmu.edu/html/departments/philosophy/Proof_Tutor.html
E-Mail: R.Scheines@andrew.cmu.edu
Architect: Wilfried Sieg, Richard Scheines
Language: Unknown
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small
87. PROTEIN
Web Page: http://www.uni-koblenz.de/ag-ki/Systems/PROTEIN/
E-Mail: peter@uni-koblenz.de
Architect: Peter Baumgartner
Language: ECLiPSe Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
88. ProveEasy
Web Page: http://www.dcs.ed.ac.uk/home/rb/
E-Mail: rb@dcs.ed.ac.uk
Architect: Rod Burstall
Language: Tcl
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
89. Prover9
Web Page: http://www.cs.unm.edu/~mccune/prover9/
E-Mail: mccune@mcs.anl.gov
Architect: William McCune
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
90. Prover, NP-Tools
Web Page: http://www.prover.com/
E-Mail: Unknown
Architect: Graeme Parkin, Gunnar Stalmarck
Language: C
Category: Theorem Prover
Interaction: Library, Logic: Classical, Size: Commercial
91. PTTP
Web Page: http://www.ai.sri.com/~stickel/pttp.html
E-Mail: stickel@ai.sri.com
Architect: Mark Stickel
Language: Common Lisp, Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
92. Purr
Web Page: http://www-cad.eecs.berkeley.edu/~cm/publications/mt/
E-Mail: cm@eecs.berkeley.edu
Architect: Christoph Meyer
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
93. PVS
  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
94. qedeq: Hilbert II
Web Page: http://www.qedeq.org/
E-Mail: mime@qedeq.org
Architect: Michael Meyling
Language: Java
Category: Proof Checker
Interaction: Batch, Logic: Classical, Size: Small
95. QuodLibet
Web Page: http://agent.informatik.uni-kl.de/quodlibet.html
E-Mail: schmidt@informatik.uni-kl.de
Architect: Ulrich Kuehler, Tobias Schmidt-Samoa, Claus-Peter Wirth
Language: Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
96. RRL
Web Page: file://cs.uiowa.edu/pub/hzhang/rrl/
E-Mail: Unknown
Architect: Hantao Zhang
Language: Zeta Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
97. Satchmo
Web Page: http://www.pms.ifi.lmu.de/software/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
98. Saturate
Web Page: http://www.mpi-sb.mpg.de/SATURATE/
E-Mail: Unknown
Architect: Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Language: Prolog
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
99. Scott
Web Page: http://users.rsise.anu.edu.au/~jks/scott.html
E-Mail: John.Slaney@anu.edu.au
Architect: John Slaney
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
100. SETHEO
Web Page: http://wwwjessen.informatik.tu-muenchen.de/~setheo/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Unknown
101. Simplify
Web Page: http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html
E-Mail: gnelson@pa.dec.com
Architect: Dave Detlefs, Greg Nelson, Jim Saxe
Language: Modula-3
Category: Theorem Prover
Interaction: Batch, Logic: Classical, Size: Small
102. Smiley
{ ! 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
103. Snark
Web Page: http://www.ai.sri.com/~stickel/snark.html
E-Mail: stickel@ai.sri.com
Architect: Mark Stickel
Language: Common Lisp
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
104. Sparkle
Web Page: http://www.cs.kun.nl/Sparkle/
E-Mail: maartenm@cs.kun.nl
Architect: Maarten de Mol
Language: Clean
Category: Tactic Prover
Interaction: Dialog, Logic: Classical, Size: Small
105. SPASS
Web Page: http://www.mpi-sb.mpg.de/units/ag2/projects/SPASS/
E-Mail: Unknown
Architect: Christoph Weidenbach
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Unknown
106. SPL
Web Page: http://www.cs.kent.ac.uk/pubs/1999/909/
E-Mail: vince@sharp.co.uk
Architect: Vincent Zammit
Language: Standard ML
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Small
107. SPRFN
Web Page: http://www.cs.unc.edu/Research/mi/mi-provers.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
108. SPTHEO
Web Page: http://wwwjessen.informatik.tu-muenchen.de/~suttner/sptheo.html
E-Mail: Unknown
Architect: Christian Suttner
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
109. SymLog
Web Page: http://www.symlog.ca/Profile/Fred.htm
E-Mail: tully@chass.utoronto.ca
Architect: Frederic Portoraro
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Classical, Size: Small
110. Tableau3
Web Page: http://logic.philosophy.ox.ac.uk/
E-Mail: floridi@ermine.ox.ac.uk
Architect: Luciano Floridi
Language: Unknown
Category: Logic Education
Interaction: Dialog, Logic: Classical, Size: Small
111. Tableaux
Web Page: http://www-formal.stanford.edu/clt/ARS/Entries/tableaux
E-Mail: Unknown
Architect: Ron Burback
Language: Unknown
Category: Proof Checker
Interaction: Editor, Logic: Classical, Size: Unknown
112. Techs: Teamwork
Web Page: http://www-avenhaus.informatik.uni-kl.de/mitarbeiter/denzinger/cooperation.html
E-Mail: denzinge@informatik.uni-kl.de
Architect: Jörg Denzinger
Language: Unknown
Category: Theorem Prover
Interaction: Script, Logic: Classical, Size: Small
113. Tecton
Web Page: http://www.cs.rpi.edu/~musser/Tecton/
E-Mail: musser@cs.rpi.edu
Architect: David Musser, Deepak Kapur
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Classical, Size: Small
114. The Logic Daemon
Web Page: http://logic.tamu.edu/daemon.html
E-Mail: colin-allen@tamu.edu
Architect: Colin Allen
Language: Perl, C
Category: Logic Education
Interaction: Batch, Logic: Classical, Size: Small
115. Theorema
Web Page: http://www.risc.uni-linz.ac.at/research/theorema/description/
E-Mail: theorema@theorema.org
Architect: Bruno Buchberger
Language: Mathematica
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Large
116. TPS
Web Page: http://gtps.math.cmu.edu/tps.html
E-Mail: Peter.Andrews@cmu.edu
Architect: Peter Andrews
Language: Common Lisp
Category: Theorem Prover
Interaction: Dialog, Logic: Classical, Size: Small
117. TPTP
    [++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
118. Universal Math Solver
Web Page: http://www.umsolver.com/
E-Mail: norths@mail.rcom.ru
Architect: Stanislav Kublanovsky
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: Classical, Size: Small
119. Vampire
Web Page: http://en.wikipedia.org/wiki/Vampire_theorem_prover
E-Mail: riazanov@cs.man.ac.uk
Architect: Andrei Voronkov, Alexandre Riazanov
Language: C++
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
120. Waldmeister
Web Page: http://www.waldmeister.org/
E-Mail: waldmeister@informatik.uni-kl.de
Architect: Arnim Buch, Thomas Hillenbrand
Language: C
Category: First Order Prover
Interaction: Script, Logic: Classical, Size: Small
121. Watson
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
122. 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
123. Z: Fuzz
Web Page: http://spivey.oriel.ox.ac.uk/mike/fuzz/
E-Mail: mike@comlab.ox.ac.uk
Architect: Mike Spivey
Language: C
Category: Representation
Interaction: Interface, Logic: Classical, Size: Large


Constructive


124. Agda
Web Page: http://www.cs.chalmers.se/~catarina/agda/
E-Mail: Unknown
Architect: Catarina Coquand
Language: Haskell
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Small
125. Coq
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
126. Coq: CtCoq
Web Page: http://www-sop.inria.fr/croap/ctcoq/ctcoq-eng.html
E-Mail: ctcoq-request@sophia.inria.fr
Architect: Yves Bertot, e.a.
Language: Unknown
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small
127. Epigram
Web Page: http://www.dur.ac.uk/CARG/epigram/
E-Mail: c.t.mcbride@durham.ac.uk
Architect: Conor McBride
Language: Haskell
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Small
128. FT
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
129. 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
130. Henk
Web Page: http://www.cse.ogi.edu/~erik/Personal/typed.htm
E-Mail: erik@cse.ogi.edu
Architect: Simon Peyton Jones, Erik Meijer
Language: Haskell
Category: Representation
Interaction: Interface, Logic: Constructive, Size: Small
131. Int
Web Page: http://class-int.narod.ru
E-Mail: urchick@mail.ru
Architect: Yuri Vtorushin, Oleg Okhotnikov
Language: C++
Category: Proof Checker
Interaction: Batch, Logic: Constructive, Size: Small
132. KIV
Web Page: http://i11www.iti.uni-karlsruhe.de/~kiv/KIV-KA.html
E-Mail: kiv-team@ira.uka.de
Architect: Unknown
Language: Lucid Common Lisp
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small
133. Kripke
++&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
134. Lambda
Web Page: http://www.cis.ksu.edu/~stough/lambda.html
E-Mail: allen@cis.ksu.edu
Architect: Allen Stoughton
Language: C
Category: Theorem Prover
Interaction: Script, Logic: Constructive, Size: Small
135. lambda Clam
Web Page: http://dream.inf.ed.ac.uk/software/lambda-clam/
E-Mail: jjb@dai.ed.ac.uk
Architect: Unknown
Language: Teyjus lambda Prolog
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small
136. lambda Prolog
Web Page: http://www.cse.psu.edu/~dale/lProlog/
E-Mail: Unknown
Architect: Dale Miller
Language: C
Category: Specification Environment
Interaction: Unknown, Logic: Constructive, Size: Small
137. Lego
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
138. Matita
Web Page: http://matita.cs.unibo.it/
Mailing List: matita-user@cs.unibo.it
Architect: Claudio Sacerdoti Coen, Andrea Asperti
Language: Objective CAML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small
139. MetaPRL
Web Page: http://metaprl.org/default.html
E-Mail: metaprl@metaprl.org
Architect: Jason Hickey, Aleksey Nogin
Language: Objective CAML
Category: Tactic Prover
Interaction: Editor, Logic: Constructive, Size: Large
140. Minlog
;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
141. Nuprl
Web Page: http://www.cs.cornell.edu/Info/Projects/NuPrl/
E-Mail: nuprl@cs.cornell.edu
Architect: Joseph Bates, Robert Constable, Stuart Allen, Douglas Howe, e.a.
Language: ML, Common Lisp
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Large
142. Oleg
Web Page: http://www.dcs.ed.ac.uk/home/ctm/oleg/quiet/
E-Mail: ctm@dcs.ed.ac.uk
Architect: Conor McBride
Language: ML
Category: Tactic Prover
Interaction: Dialog, Logic: Constructive, Size: Small
143. PhoX
Web Page: http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html
Mailing List: af2@logique.jussieu.fr
Architect: Christophe Raffalli
Language: Objective CAML
Category: Tactic Prover
Interaction: Script, Logic: Constructive, Size: Small
144. Plastic
 [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
145. Porgi
Web Page: http://www.cis.ksu.edu/~stough/porgi.html
E-Mail: allen@cis.ksu.edu
Architect: Allen Stoughton
Language: Standard ML of New Jersey
Category: Theorem Prover
Interaction: Script, Logic: Constructive, Size: Small
146. Proof
Web Page: http://www.keyfitz.org/jburdick/
E-Mail: jburdick@gradient.cis.upenn.edu
Architect: Josh Burdick
Language: Java
Category: Proof Checker
Interaction: Script, Logic: Constructive, Size: Small
147. Tutch
  [ 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
148. 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
149. 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


None


150. Axiom
Web Page: http://www.axiom-developer.org
E-Mail: daly@axiom-developer.org
Architect: Richard Jenks, Robert Sutor
Language: Common Lisp, C, Boot, Spad
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
151. bc
Web Page: http://www.gnu.org/software/bc/
E-Mail: Unknown
Architect: Unknown
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
152. calc
Web Page: http://www.numbertheory.org/calc/krm_calc.html
E-Mail: krm@maths.uq.edu.au
Architect: Unknown
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
153. Cocoa
Web Page: http://cocoa.dima.unige.it/
E-Mail: cocoa@dima.unige.it
Architect: Antonio Capani, Gianfranco Niesi
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
154. CREP
Web Page: http://www.mathematik.uni-bielefeld.de/~sek/crep.html
E-Mail: fdowner@mathematik.uni.bielefeld.de
Architect: Peter Dräxler
Language: Pascal, C, Java, Maple
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
155. Derive
Web Page: http://en.wikipedia.org/wiki/Derive_computer_algebra_system
E-Mail: Unknown
Architect: David Stoutemyer, Albert Rich
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
156. Equplus
Web Page: http://equplus.net/
E-Mail: Unknown
Architect: Maria Chernenko
Language: Unknown
Category: Information
Interaction: Corpus, Logic: None, Size: Small
157. Expressionist
Web Page: http://www.livemath.com/matheq/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
158. Fermat
Web Page: http://www.bway.net/~lewis/
E-Mail: rlewis@fordham.edu
Architect: Robert Lewis
Language: Pascal
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
159. Form
Web Page: http://www.nikhef.nl/~form/
E-Mail: Unknown
Architect: Jos Vermaseren
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
160. FriCAS
Web Page: http://fricas.sourceforge.net/
E-Mail: fricas-devel@googlegroups.com
Architect: Richard Jenks, Robert Sutor
Language: Common Lisp, C, Boot, Spad
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
161. Gb/FGb, RS
Web Page: http://fgbrs.lip6.fr/
E-Mail: jcf@calfor.lip6.fr
Architect: Jean-Charles Faugère
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: None, Size: Small
162. Giac/xcas
Web Page: http://www-fourier.ujf-grenoble.fr/~parisse/english.html
E-Mail: parisse@fourier.ujf-grenoble.fr
Architect: Bernard Parisse
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
163. GiNaC
Web Page: http://www.ginac.de/
Mailing List: ginac-list@ginac.de
Architect: Christian Bauer, Alexander Frink, Richard Kreckel
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
164. HDM
\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
165. JACAL
Web Page: http://swiss.csail.mit.edu/~jaffer/JACAL
E-Mail: agj@alum.mit.edu
Architect: Aubrey Jaffer
Language: Scheme
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
166. JavaMath
Web Page: http://javamath.sourceforge.net/
E-Mail: javamath-support@lists.sourceforge.net
Architect: Andrew Solomon, Craig Struble
Language: Java
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
167. KANT/KASH
Web Page: http://www.math.tu-berlin.de/~kant/kash.html
E-Mail: kant@math.tu-berlin.de
Architect: Michael Pohst
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
168. Leda
Web Page: http://www.mpi-sb.mpg.de/LEDA/
E-Mail: Unknown
Architect: Stefan Näher
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Unknown
169. LiDIA
Web Page: http://www.cdc.informatik.tu-darmstadt.de/TI/LiDIA/
Mailing List: LiDIA-request@cdc.informatik.tu-darmstadt.de
Architect: Unknown
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
170. LiveMath
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
171. LLF
Web Page: http://theory.stanford.edu/~iliano/LLF/LLF.html
E-Mail: iliano@cs.stanford.edu
Architect: Iliano Cervesato
Language: ML
Category: Proof Checker
Interaction: Batch, Logic: None, Size: Small
172. Macaulay
Web Page: http://www.math.uiuc.edu/Macaulay2/
E-Mail: Unknown
Architect: Daniel Grayson, Michael Stillman
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Unknown
173. Macsyma
Web Page: http://www.macsyma.com/
E-Mail: Unknown
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
174. Macsyma: Maxima
Web Page: http://maxima.sourceforge.net/
Mailing List: maxima@math.utexas.edu
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
175. Macsyma: Punimax
Web Page: http://symbolicnet.mcs.kent.edu/systems/macsyma.html
E-Mail: Unknown
Architect: Joel Moses, e.a.
Language: Common Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
176. Magma
Web Page: http://magma.maths.usyd.edu.au/
E-Mail: magma@maths.usyd.edu.au
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Script, Logic: None, Size: Commercial
177. Maple
Web Page: http://www.maplesoft.com/
E-Mail: sales_info@maplesoft.com
Architect: Keith Geddes, Gaston Gonnet, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
178. Mathcad
Web Page: http://www.mathcad.com/mathcad/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
179. Mathematica
Web Page: http://www.wolfram.com/products/mathematica/index.html
E-Mail: info@wolfram.com
Architect: Stephen Wolfram, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
180. Mathematica: Publicon
Web Page: http://www.wolfram.com/products/publicon/index.html
E-Mail: info@publicon.com
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
181. MathScript
Web Page: http://www.mathscript.pair.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
182. MathView
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
183. Merill
Web Page: ftp://ftp.dcs.glasgow.ac.uk/pub/merill/
E-Mail: Unknown
Architect: Brian Matthews
Language: Standard ML
Category: Specification Environment
Interaction: Dialog, Logic: None, Size: Small
184. MuPAD
Web Page: http://www.mupad.de/
E-Mail: Unknown
Architect: Benno Fuchssteiner, e.a.
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
185. nauty
Web Page: http://cs.anu.edu.au/~bdm/nauty/
E-Mail: bdm@cs.anu.edu.au
Architect: Brendan D. McKay
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
186. NTL
Web Page: http://www.cs.wisc.edu/~shoup/ntl/
E-Mail: shoup@cs.wisc.edu
Architect: Victor Shoup
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
187. OpenMath
        </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
188. Pari/GP
Web Page: http://pari.math.u-bordeaux.fr/
E-Mail: pari@math.u-bordeaux.fr
Architect: Henri Cohen
Language: C
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
189. polymake
Web Page: http://www.math.tu-berlin.de/polymake/
E-Mail: polymake@math.tu-berlin.de
Architect: Ewgenij Gawrilow, Michael Joswig
Language: C++
Category: Computer Algebra
Interaction: Script, Logic: None, Size: Small
190. Reduce
Web Page: http://www.uni-koeln.de/REDUCE/
E-Mail: Unknown
Architect: Tony Hearn
Language: Standard Lisp
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
191. ring.perisic.com
Web Page: http://ring.perisic.com/
E-Mail: marc@pension-perisic.de
Architect: Marc Conrad
Language: Java
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
192. Rotater
Web Page: http://casr.adelaide.edu.au/rotater/
E-Mail: craig@raru.adelaide.edu.au
Architect: Craig Kloeden
Language: C
Category: Computer Algebra
Interaction: Editor, Logic: None, Size: Small
193. SACLIB
Web Page: http://www.cis.udel.edu/~saclib/
Mailing List: saclib-l@risc.uni-linz.ac.at
Architect: George E. Collins, Hoon Hong
Language: C
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
194. Schoonschip
Web Page: ftp://archive.umich.edu/physics/schip/
E-Mail: Unknown
Architect: Martin Veltman
Language: 68000 Assembly
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
195. Scilab
Web Page: http://www.scilab.org/
E-Mail: Unknown
Architect: Unknown
Language: C, Fortran
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
196. Singular
Web Page: http://www.singular.uni-kl.de/
E-Mail: singular@mathematik.uni-kl.de
Architect: Unknown
Language: C, C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
197. Swift
Web Page: http://www.geocities.com/SiliconValley/Heights/5445/survey.html
E-Mail: Unknown
Architect: P S Karthikeyan, P S Ranganathan
Language: Java
Category: Authoring
Interaction: Editor, Logic: None, Size: Small
198. SYNAPS
Web Page: http://www-sop.inria.fr/galaad/logiciels/synaps/
E-Mail: mourrain@sophia.inria.fr
Architect: Unknown
Language: C++
Category: Computer Algebra
Interaction: Library, Logic: None, Size: Small
199. Techexplorer
Web Page: http://www.software.ibm.com/network/techexplorer/
E-Mail: techexpl@us.ibm.com
Architect: Robert Sutor, Angel Diaz
Language: C++
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
200. TeX: LaTeX
\[(-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
201. 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
202. Yacas
Web Page: http://yacas.sourceforge.net/
E-Mail: Unknown
Architect: Ayal Pinkus
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small


Unknown


203. Acela
Web Page: http://homepages.cwi.nl/~steven/acela/
E-Mail: steven@cwi.nl
Architect: Arjeh Cohen, Lambert Meertens
Language: HTML
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small
204. ActiveMath
Web Page: http://www.mathweb.org/activemath/
E-Mail: melis@ags.uni-sb.de
Architect: Erica Melis
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
205. Aldor
Web Page: http://www.aldor.org/
E-Mail: Stephen.Watt@sophia.inria.fr
Architect: Stephen Watt
Language: C
Category: Computer Algebra
Interaction: Batch, Logic: Unknown, Size: Small
206. Amphion
Web Page: http://ase.arc.nasa.gov/docs/amphion.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
207. B Method: Atelier B
Web Page: http://www.atelierb.societe.com/
E-Mail: maintenance.atelierb@clearsy.com
Architect: Jean-Raymond Abrial
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial
208. B Method: B4free
Web Page: http://www.b4free.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
209. B Method: Click'n'Prove
Web Page: http://www.loria.fr/~cansell/cnp.html
E-Mail: cansell@lloria.fr
Architect: Jean-Raymond Abrial, Dominique Cansell
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
210. CafeOBJ
Web Page: http://www.ldl.jaist.ac.jp/cafeobj/
E-Mail: Unknown
Architect: Kokichi Futatsugi
Language: Common Lisp
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
211. Calculemus
Web Page: http://www.mathweb.org/calculemus/
Mailing List: calculemus-ig@ags.uni-sb.de
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
212. CASL
Web Page: http://www.cofi.info/CASL.html
E-Mail: pdmosses@brics.dk
Architect: Michel Bidoit, Peter D. Mosses
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
213. Caveat
Web Page: http://www-list.cea.fr/gb/programmes/sys_embarques/labo_lsl/caveat/index_caveat_gb.htm
E-Mail: Jacques.Raguideau@cea.fr
Architect: Unknown
Language: C, C++
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial
214. CCR: RDL
Web Page: http://www.mrg.dist.unige.it/ccr/
E-Mail: silvio@dist.unige.it
Architect: Alessandro Armando, Silvio Ranise
Language: SICStus Prolog
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small
215. CL
Web Page: http://www.ii.fmph.uniba.sk/~voda/cl.html
E-Mail: voda@fmph.uniba.sk
Architect: Paul Voda
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small
216. Coral
Web Page: http://dream.inf.ed.ac.uk/projects/coral/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
217. Deduktion
Web Page: http://www.uni-koblenz.de/ag-ki/Deduktion/
E-Mail: peter@informatik.uni-koblenz.de
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
218. Deva: Devil
Web Page: http://swt.cs.tu-berlin.de/~ma/devil/index.html
E-Mail: ma@first.gmd.de
Architect: Matthias Anlauff
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small
219. DFG
Web Page: http://www.uni-koblenz.de/ag-ki/Deduktion/#OtherActivities
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
220. Dimacs
Web Page: ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/satformat.tex
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Unknown, Size: Small
221. Discount
Web Page: http://www.uni-kl.de/AG-AvenhausMadlener/discount.html
E-Mail: denzinge@informatik.uni-kl.de
Architect: Jörg Denzinger
Language: Unknown
Category: Theorem Prover
Interaction: Script, Logic: Unknown, Size: Small
222. DPL: CN D
Web Page: http://www.ai.mit.edu/projects/dynlangs/Projects/DPL.htm
E-Mail: koud@ai.mit.edu
Architect: Kostas Arkoudas
Language: ML
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small
223. DTP
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/dtp/0.html
E-Mail: Unknown
Architect: Don Geddis
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
224. ELAN
Web Page: http://www.loria.fr/equipes/protheo/PROJECTS/ELAN/elan.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Unknown
225. Ergo
Web Page: http://www.itee.uq.edu.au/~pjr/HomePages/ErgoHome.html
E-Mail: Unknown
Architect: Peter Robinson, e.a.
Language: Qu Prolog
Category: Tactic Prover
Interaction: Unknown, Logic: Unknown, Size: Small
226. Esterel
Web Page: http://www.esterel-technologies.com/
Mailing List: esterel-users@sophia.inria.fr
Architect: Gérard Berry
Language: Esterel
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
227. Evidence Algorithm: SAD
Web Page: http://ea.unicyb.kiev.ua/sad.en.html
E-Mail: lav@unicyb.kiev.ua
Architect: Andrey Paskevich
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small
228. Evolver
Web Page: http://www.susqu.edu/facstaff/b/brakke/evolver/evolver.html
E-Mail: brakke@susqu.edu
Architect: Ken Brakke
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
229. EzMath
Web Page: http://www.w3.org/People/Raggett/EzMath/
E-Mail: Unknown
Architect: Dave Raggett
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small
230. Fiesta
Web Page: http://www.cs.miami.edu/~tptp/CASC/16/SystemDescriptions.html#Fiesta
E-Mail: roberto@lsi.upc.es
Architect: Robert Nieuwenhuis
Language: Unknown
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small
231. Focal
Web Page: http://focal.inria.fr/site/index.php
E-Mail: therese.hardin@lip6.fr
Architect: Thérèse Hardin, Renaud Rioboo
Language: Objective CAML
Category: Computer Algebra
Interaction: Library, Logic: Unknown, Size: Small
232. foetus
Web Page: http://www.informatik.uni-muenchen.de/~abel/publications/foetus/
E-Mail: abel@informatik.uni-muenchen.de
Architect: Andreas Abel
Language: Standard ML
Category: Specification Environment
Interaction: Batch, Logic: Unknown, Size: Small
233. FOL
Web Page: http://www-formal.stanford.edu/pub/FOL/home.html
E-Mail: rww@sail.stanford.edu
Architect: Richard Weyhrauch, Carolyn Talcott
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
234. Formal Methods Page
Web Page: http://www.onlinecomputersciencedegree.com/resources/formal-methods/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
235. Formal Methods Wiki
Web Page: http://formalmethods.wikia.com/
E-Mail: jonathan.bowen@lsbu.ac.uk
Architect: Jonathan Bowen
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
236. Forum
Web Page: http://www.lix.polytechnique.fr/Labo/Dale.Miller/forum/
E-Mail: Unknown
Architect: Dale Miller
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
237. Frapps
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/frapps/0.html
E-Mail: Unknown
Architect: Alan Frisch, Tomas Uribe, Michael Mitchell
Language: Common Lisp
Category: First Order Prover
Interaction: Unknown, Logic: Unknown, Size: Small
238. GAP
Web Page: http://www-gap.dcs.st-and.ac.uk/~gap/
E-Mail: gap@dcs.st-and.ac.uk
Architect: Martin Schönert, e.a.
Language: C
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Large
239. Geometry Expert
Web Page: http://en.wikipedia.org/wiki/Geometry_Expert
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
240. Graffiti
Web Page: http://www.math.uh.edu/~clarson/graffiti.html
E-Mail: MATH0@Jetson.UH.EDU
Architect: Siemion Fajtlowicz
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
241. Graph Theorist
Web Page: http://www.cs.hunter.cuny.edu/~epstein/html/gt.html
E-Mail: susan.epstein@hunter.cuny.edu
Architect: Susan Epstein
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
242. Guru
Web Page: http://code.google.com/p/guru-lang/
E-Mail: astump@acm.org
Architect: Aaron Stump
Language: Java
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
243. Helena
Web Page: http://helm.cs.unibo.it/lambda_delta/
E-Mail: fguidi@cs.unibo.it
Architect: Ferruccio Guidi
Language: Objective CAML
Category: Proof Checker
Interaction: Batch, Logic: Unknown, Size: Small
244. Helm
Web Page: http://helm.cs.unibo.it/
E-Mail: asperti@cs.unibo.it
Architect: Andrea Asperti
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
245. Hiper
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/hiper/0.html
E-Mail: Unknown
Architect: Jim Christian
Language: Common Lisp
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
246. HR
Web Page: http://www.dai.ed.ac.uk/daidb/people/homes/simonco/research/hr/
E-Mail: simonco@dai.ed.ac.uk
Architect: Simon Colton
Language: Unknown
Category: Theorem Prover
Interaction: Batch, Logic: Unknown, Size: Small
247. IDA: Algebra Interactive
Web Page: http://www.win.tue.nl/~ida/
E-Mail: Unknown
Architect: Arjeh Cohen, Hans Cuypers, Hans Sterk
Language: HTML
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Small
248. ILF
Web Page: http://www.uni-koblenz.de/~dahn/index-Dateien/Page425.htm
E-Mail: ilfserv-request@mathematik.hu-berlin.de
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
249. IMP
Web Page: http://www.uclic.ucl.ac.uk/imp/
E-Mail: j.gow@ucl.ac.uk
Architect: Paul Cairns, Jeremy Gow
Language: XSL
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
250. IPR
(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
251. ISO 12083
Web Page: http://www.oasis-open.org/cover/gen-apps.html#iso12083DTDs
E-Mail: Unknown
Architect: Eric van Herwijnen
Language: SGML
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Unknown
252. ITP
Web Page: http://www.dcs.gla.ac.uk/~stuart/ITP/ITP.html
E-Mail: Unknown
Architect: Stuart Aitken, Tom Melham, Muffy Calder, Phil Gray
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
253. Keim
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/keim/0.html
E-Mail: Unknown
Architect: Dan Nesmith, Jörg Siekman
Language: Common Lisp, CLOS
Category: Theorem Prover
Interaction: Library, Logic: Unknown, Size: Unknown
254. KIDS
Web Page: http://www.kestrel.edu/home/prototypes/kids.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
255. Leibniz
Web Page: http://www.utdallas.edu/~klaus/Leibnizprogram/leibnizmain.html
E-Mail: klaus@utdallas.edu
Architect: Klaus Truemper
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
256. llprover
Web Page: http://bach.seg.kobe-u.ac.jp/llprover/
E-Mail: tamura@kobe-u.ac.jp
Architect: Naoyuki Tamura
Language: SICStus Prolog
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small
257. Logic Animations
Web Page: http://turing.wins.uva.nl/~jaspars/animations/
E-Mail: jaspars@wins.uva.nl
Architect: Jan Jaspars
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Unknown, Size: Small
258. Logic Broker Architecture
Web Page: http://www.mathweb.org/calculemus/meetings/standrews00/armando.abstract
E-Mail: armando@mrg.dist.unige.it
Architect: Alessandro Armando, Daniele Zini
Language: Unknown
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
259. Logosphere
Web Page: http://www.logosphere.org/
Mailing List: logosphere-developer@cs.yale.edu
Architect: Carsten Schürmann
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
260. Map: Logiweb
Web Page: http://yoa.dk/
E-Mail: grue@diku.dk
Architect: Klaus Grue
Language: Unknown
Category: Proof Checker
Interaction: Unknown, Logic: Unknown, Size: Small
261. MathCaffeine
Web Page: http://atlas-conferences.com/c/a/e/e/48.htm
E-Mail: asvern@essex.ac.uk
Architect: Alexei Vernitski
Language: Unknown
Category: Authoring
Interaction: Unknown, Logic: Unknown, Size: Small
262. MathLive
Web Page: http://www.milohedge.com/products/mathlive/mathlive.html
E-Mail: info@milohedge.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial
263. MathML
Web Page: http://www.w3.org/Math/mathml-faq.html
E-Mail: Unknown
Architect: Unknown
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Unknown
264. MathPad
Web Page: http://pubpages.unh.edu/~mwidholm/MathPad/
E-Mail: Mark.Widholm@UNH.edu
Architect: Mark Widholm
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
265. Mathtools
Web Page: http://www.mathtools.net/
E-Mail: feedback@mathtools.net
Architect: Ophir Herbst
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
266. MathWeb: Mosh
Web Page: http://www.mathweb.org/mathweb/
E-Mail: afranke@ags.uni-sb.de
Architect: Andreas Franke, Michael Kohlhase
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
267. Matlab
Web Page: http://www.mathworks.com/products/matlab/
E-Mail: info@mathworks.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial
268. Maude
Web Page: http://maude.cs.uiuc.edu/
Mailing List: maude-users@maude.cs.uiuc.edu
Architect: José Meseguer
Language: Maude
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial
269. MBase
Web Page: http://www.mathweb.org/mbase/
E-Mail: kohlhase@cs.uni-sb.de
Architect: Andreas Franke, Michael Kohlhase
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Unknown, Size: Small
270. Minitab
Web Page: http://www.minitab.com/
E-Mail: sales@minitab.com
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Commercial
271. MINSE
Web Page: http://lfw.org/math/
E-Mail: Unknown
Architect: Ka-Ping Yee
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
272. MoWGLI
Web Page: http://www.mowgli.cs.unibo.it/
E-Mail: asperti@cs.unibo.it
Architect: Andrea Asperti
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
273. MuTTI
Web Page: http://www.tcs.informatik.uni-muenchen.de/mitarbeiter/alti/index.html
E-Mail: alti@informatik.uni-muenchen.de
Architect: Thorsten Altenkirch
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small
274. MVL
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/mvl/0.html
E-Mail: Unknown
Architect: Matthew Ginsberg
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
275. NewPandora
Web Page: http://www.doc.ic.ac.uk/~kb/#Pandora
E-Mail: kb@doc.ic.ac.uk
Architect: Krysia Broda
Language: Unknown
Category: Logic Education
Interaction: Unknown, Logic: Unknown, Size: Small
276. OMDoc
Web Page: http://www.mathweb.org/omdoc/
E-Mail: kohlhase+@cs.cmu.edu
Architect: Michael Kohlhase
Language: XML
Category: Representation
Interaction: Unknown, Logic: Unknown, Size: Small
277. Omega: OAnts
Web Page: http://www.ags.uni-sb.de/~omega/index.php?target=publications&ref=C8
E-Mail: chris@ags.uni-sb.de
Architect: Christoph Benzmüller, Volker Sorge
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
278. OMRS
Web Page: http://www.kestrel.edu/home/people/coglio/ids98.ps
E-Mail: fausto@itc.it
Architect: Fausto Giunchiglia, Carolyn Talcott, Alessandro Armando
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
279. OpenXM
Web Page: http://www.math.s.kobe-u.ac.jp/OpenXM/
E-Mail: takayama@math.sci.kobe-u.ac.jp
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
280. ORA Canada Biblography of Automated Deduction
Web Page: http://www.ora.on.ca/biblio/biblio-prover-welcome.html
E-Mail: Unknown
Architect: Bill Pase, Karen Summerskill
Language: Unknown
Category: Information
Interaction: Corpus, Logic: Unknown, Size: Small
281. Oscar
Web Page: http://www.u.arizona.edu/~pollock/
E-Mail: Unknown
Architect: John Pollock
Language: Common Lisp
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
282. Perfect Developer
Web Page: http://www.eschertech.com/products/index.php
E-Mail: sales@eschertech.com
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Commercial
283. Plural
Web Page: http://www.singular.uni-kl.de/plural/
E-Mail: Unknown
Architect: Gert-Martin Greuel, Viktor Levandovskyy, Hans Schönemann
Language: C, C++
Category: Computer Algebra
Interaction: Dialog, Logic: Unknown, Size: Small
284. ProofPad
Web Page: http://www-irm.mathematik.hu-berlin.de/~ilf/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
285. Prosper
Web Page: http://www.dcs.gla.ac.uk/prosper/
E-Mail: tfm@dcs.gla.ac.uk
Architect: T.F. Melham
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
286. QED Project
Web Page: http://www-unix.mcs.anl.gov/qed/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Information
Interaction: Interface, Logic: Unknown, Size: Small
287. QED Pro Quo
Web Page: http://www.qpq.org/
E-Mail: kohlhase+@cs.cmu.edu
Architect: Michael Kohlhase, Sam Owre, Natarajan Shankar
Language: Unknown
Category: Information
Interaction: Unknown, Logic: Unknown, Size: Small
288. REDLOG
Web Page: http://www.fmi.uni-passau.de/~redlog/
E-Mail: redlog@fmi.uni-passau.de
Architect: Andreas Dolzmann, Thomas Sturm
Language: Unknown
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
289. Risa/Asir
Web Page: http://www.asir.org/
E-Mail: takesima@flab.fujitsu.co.jp
Architect: Unknown
Language: C, Assembly
Category: Computer Algebra
Interaction: Dialog, Logic: Unknown, Size: Small
290. Safelogic Verifier
Web Page: http://www.jasper-da.com/products_jaspergold.htm
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
291. SEM
Web Page: http://www.cs.uiowa.edu/~hzhang/sem.html
E-Mail: hzhang@cs.uiowa.edu
Architect: Unknown
Language: Unknown
Category: First Order Prover
Interaction: Unknown, Logic: Unknown, Size: Small
292. Senac
Web Page: http://www.can.nl/SystemsOverview/General/SENAC/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Unknown
293. SIMATH
Web Page: http://emmy.math.uni-sb.de/~simath/
E-Mail: simath@math.uni-sb.de
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
294. Specware
Web Page: http://www.kestrel.edu/home/prototypes/specware.html
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Editor, Logic: Unknown, Size: Small
295. STeP
Web Page: http://www-step.stanford.edu/
E-Mail: step-comments@cs.stanford.edu
Architect: Zohar Manna, Henny Sipma
Language: Unknown
Category: Specification Environment
Interaction: Dialog, Logic: Unknown, Size: Small
296. SuchThat
Web Page: http://www.cs.rpi.edu/~schupp/suchthat/#verificat
E-Mail: schupp@cs.rpi.edu
Architect: Sibylle Schupp, Rüdiger Loos
Language: Unknown
Category: Computer Algebra
Interaction: Unknown, Logic: Unknown, Size: Small
297. Sunrise
Web Page: http://www.cis.upenn.edu/~hol/sunrise/
E-Mail: homeier@saul.cis.upenn.edu
Architect: Peter Homeier
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
298. SVC
Web Page: http://verify.stanford.edu/SVC/
E-Mail: SVC@verify.stanford.edu
Architect: Jeremy Levitt
Language: C++
Category: Theorem Prover
Interaction: Unknown, Logic: Unknown, Size: Small
299. VDM
Web Page: http://www.csr.ncl.ac.uk/vdm/
E-Mail: John.Fitzgerald@ncl.ac.uk
Architect: Unknown
Language: Unknown
Category: Specification Environment
Interaction: Unknown, Logic: Unknown, Size: Small
300. WebEQ
Web Page: http://www.dessci.com/en/
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Commercial
301. XPNet
Web Page: http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/reasonng/atp/systems/xpnet/0.html
E-Mail: Unknown
Architect: Jawahar Chirimar, Carl Gunter, Myra VanInwegen
Language: Unknown
Category: Proof Checker
Interaction: Editor, Logic: Unknown, Size: Small
302. Zenon
Web Page: http://focal.inria.fr/zenon/
E-Mail: damien.doligez@inria.fr
Architect: Damien Doligez
Language: Objective CAML
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small