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