--- a/auto-proof.rst	Wed Apr 15 23:48:56 2009 +0300
+++ b/auto-proof.rst	Thu Apr 16 21:18:40 2009 +0300
@@ -1,5 +1,12 @@
 -*- outline -*-
 
+* Info/links.
+
+See
+
+  http://en.wikipedia.org/wiki/Automated_theorem_proving
+
+
 * proofgeneral.
 
   $ sudo apt-get install proofgeneral
@@ -65,3 +72,41 @@
 See
 
   http://formalmath.tiddlyspot.com/
+
+* PVS Specification and Verification System
+
+Old (1992). The system is implemented in Common Lisp, and is released under
+the GNU General Public License (GPL).
+
+See
+
+  http://pvs.csl.sri.com/
+  http://en.wikipedia.org/wiki/Prototype_Verification_System
+  http://www-formal.stanford.edu/clt/ARS/Entries/pvs
+
+* The TPTP Problem Library for Automated Theorem Proving.
+
+The TPTP (Thousands of Problems for Theorem Provers) is a library of test
+problems for automated theorem proving (ATP) systems. The TPTP supplies the
+ATP community with:
+
+ * A comprehensive library of the ATP test problems that are available today,
+   in order to provide an overview and a simple, unambiguous reference
+   mechanism.
+ * A comprehensive list of references and other interesting information for
+   each problem.
+ * Arbitrary size instances of generic problems (e.g., the N-queens problem).
+ * A utility to convert the problems to existing ATP systems' formats.
+ * General guidelines outlining the requirements for ATP system evaluation.
+ * Standards for input and output for ATP systems.
+
+The principal motivation for the TPTP is to support the testing and evaluation
+of ATP systems, to help ensure that performance results accurately reflect the
+capabilities of the ATP system being considered. A common library of problems
+is necessary for meaningful system evaluations, meaningful system comparisons,
+repeatability of testing, and the production of statistically significant
+results. The TPTP is such a library.
+
+See
+
+  http://www.cs.miami.edu/~tptp/