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 size of the effort. 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 logic that is supported. 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.




Commercial


1. 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
2. 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
3. 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
4. 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
5. Expressionist
Web Page: http://www.livemath.com/matheq/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
6. 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
7. LiveMath
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
8. 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
9. 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
10. 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
11. 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
12. Mathcad
Web Page: http://www.mathcad.com/mathcad/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Commercial
13. 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
14. 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
15. 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
16. MathScript
Web Page: http://www.mathscript.pair.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Authoring
Interaction: Editor, Logic: None, Size: Commercial
17. 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
18. 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
19. 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
20. 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
21. 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
22. 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
23. 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
24. 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
25. 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
26. 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
27. WebEQ
Web Page: http://www.dessci.com/en/
E-Mail: Unknown
Architect: Unknown
Language: Java
Category: Authoring
Interaction: Editor, Logic: Unknown, Size: Commercial


Large


28. 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
29. 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
30. 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
31. 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
32. 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
33. 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
34. 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
35. 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
36. 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
37. 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
38. 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
39. 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
40. 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
41. 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
42. 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
43. 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
44. 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
45. 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
46. 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
47. 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
48. 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
49. 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
50. 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
51. Scilab
Web Page: http://www.scilab.org/
E-Mail: Unknown
Architect: Unknown
Language: C, Fortran
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Large
52. 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
53. 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
54. 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
55. Z: Fuzz
Web Page: http://spivey.oriel.ox.ac.uk/mike/fuzz/
E-Mail: mike@comlab.ox.ac.uk
Architect: Mike Spivey
Language: C
Category: Representation
Interaction: Interface, Logic: Classical, Size: Large


Small


56. 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
57. 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
58. 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
59. 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
60. 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
61. 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
62. Alfie
Web Page: http://www.cs.chalmers.se/~sydow/alfie/index.html
E-Mail: Unknown
Architect: Björn von Sydow
Language: Haskell
Category: Logic Education
Interaction: Editor, Logic: Classical, Size: Small
63. 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
64. 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
65. 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
66. 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
67. 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
68. 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
69. 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
70. 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
71. 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
72. 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
73. 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
74. 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
75. 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
76. 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
77. 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
78. 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
79. 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
80. 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
81. 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
82. 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
83. 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
84. 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
85. 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
86. 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
87. 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
88. 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
89. 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
90. 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
91. 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
92. 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
93. 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
94. 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
95. 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
96. 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
97. 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
98. 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
99. 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
100. 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
101. 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
102. 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
103. 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
104. 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
105. 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
106. Equplus
Web Page: http://equplus.net/
E-Mail: Unknown
Architect: Maria Chernenko
Language: Unknown
Category: Information
Interaction: Corpus, Logic: None, Size: Small
107. 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
108. 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
109. 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
110. 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
111. 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
112. 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
113. 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
114. 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
115. 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
116. 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
117. 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
118. 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
119. 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
120. 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
121. 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
122. 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
123. 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
124. 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
125. 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
126. 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
127. 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
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. 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
130. 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
131. 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
132. 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
133. 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
134. 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
135. 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
136. 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
137. 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
138. 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
139. 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
140. 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
141. 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
142. 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
143. 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
144. 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
145. 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
146. 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
147. 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
148. 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
149. 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
150. 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
151. 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
152. 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
153. 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
154. 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
155. 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
156. 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
157. 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
158. 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
159. 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
160. 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
161. 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
162. 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
163. 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
164. 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
165. 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
166. 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
167. 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
168. 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
169. 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
170. 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
171. 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
172. 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
173. 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
174. 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
175. 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
176. 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
177. 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
178. llprover
Web Page: http://bach.seg.kobe-u.ac.jp/llprover/
E-Mail: tamura@kobe-u.ac.jp
Architect: Naoyuki Tamura
Language: SICStus Prolog
Category: First Order Prover
Interaction: Script, Logic: Unknown, Size: Small
179. 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
180. 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
181. 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
182. 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
183. 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
184. 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
185. 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
186. 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
187. 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
188. 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
189. 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
190. 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
191. 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
192. MathView
Web Page: http://www.livemath.com/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
193. 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
194. 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
195. MBase
Web Page: http://www.mathweb.org/mbase/
E-Mail: kohlhase@cs.uni-sb.de
Architect: Andreas Franke, Michael Kohlhase
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Unknown, Size: Small
196. 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
197. 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
198. 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
199. 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
200. MINSE
Web Page: http://lfw.org/math/
E-Mail: Unknown
Architect: Ka-Ping Yee
Language: Unknown
Category: Representation
Interaction: Interface, Logic: Unknown, Size: Small
201. 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
202. 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
203. 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
204. 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
205. 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
206. 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
207. 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
208. 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
209. 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
210. 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
211. 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
212. 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
213. 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
214. 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
215. 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
216. 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
217. 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
218. 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
219. 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
220. 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
221. 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
222. 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
223. 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
224. 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
225. 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
226. 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
227. 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
228. 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
229. 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
230. 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
231. 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
232. 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
233. 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
234. 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
235. 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
236. 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
237. 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
238. 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
239. 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
240. 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
241. 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
242. 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
243. 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
244. 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
245. 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
246. 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
247. 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
248. 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
249. 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
250. 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
251. 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
252. 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
253. 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
254. 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
255. 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
256. 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
257. 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
258. 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
259. 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
260. 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
261. 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
262. 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
263. 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
264. 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
265. 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
266. 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
267. 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
268. 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
269. 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
270. 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
271. 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
272. 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
273. 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
274. 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
275. 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
276. 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
277. 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
278. 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
279. 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
280. 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
281. 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
282. 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
283. 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
284. 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
285. 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
286. Yacas
Web Page: http://yacas.sourceforge.net/
E-Mail: Unknown
Architect: Ayal Pinkus
Language: C++
Category: Computer Algebra
Interaction: Dialog, Logic: None, Size: Small
287. 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
288. 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


Unknown


289. DReaM
Web Page: http://dream.inf.ed.ac.uk/
E-Mail: Unknown
Architect: Unknown
Language: Unknown
Category: Representation
Interaction: Corpus, Logic: Classical, Size: Unknown
290. 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
291. 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
292. 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
293. 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
294. 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
295. 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
296. 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
297. 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
298. 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
299. 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
300. 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
301. 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
302. 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