# HG changeset patch
# User Oleksandr Gavenko <gavenkoa@gmail.com>
# Date 1239906265 -10800
# Node ID bd52334e3a992adcb7ef82890b3a3dc976c999c9
# Parent  716febef618843fe0afd209065d30be09cc21e8d
pvs correction.

diff -r 716febef6188 -r bd52334e3a99 auto-proof.rst
--- a/auto-proof.rst	Thu Apr 16 21:18:40 2009 +0300
+++ b/auto-proof.rst	Thu Apr 16 21:24:25 2009 +0300
@@ -75,8 +75,10 @@
 
 * PVS Specification and Verification System
 
-Old (1992). The system is implemented in Common Lisp, and is released under
-the GNU General Public License (GPL).
+Old (1992). Many article in 199x.
+
+The system is implemented in Common Lisp, and is released under the GNU
+General Public License (GPL).
 
 See
 
@@ -110,3 +112,11 @@
 See
 
   http://www.cs.miami.edu/~tptp/
+
+* SPASS.
+
+An Automated Theorem Prover for First-Order Logic with Equality.
+
+See
+
+  http://www.spass-prover.org/index.html