auto-proof.rst
changeset 2228 837f1337c59b
parent 1912 8b81a8f0f692
--- a/auto-proof.rst	Sat Feb 10 01:28:53 2018 +0200
+++ b/auto-proof.rst	Sat Feb 10 01:30:24 2018 +0200
@@ -9,7 +9,7 @@
 Info/links
 ==========
 
- * http://en.wikipedia.org/wiki/Automated_theorem_proving
+* http://en.wikipedia.org/wiki/Automated_theorem_proving
 
 proofgeneral
 ============
@@ -32,7 +32,7 @@
 
 See:
 
- * http://proofgeneral.inf.ed.ac.uk/
+* http://proofgeneral.inf.ed.ac.uk/
 
 Isabelle
 ========
@@ -48,8 +48,8 @@
 
 See:
 
- * http://isabelle.in.tum.de/overview.html
- * http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
+* http://isabelle.in.tum.de/overview.html
+* http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
 
 IsarMathLib
 ===========
@@ -60,12 +60,12 @@
 
 See:
 
-  http://isarmathlib.org/
-    Home page
-  http://savannah.nongnu.org/projects/isarmathlib
-    Project page
-  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
-    Mail list
+http://isarmathlib.org/
+  Home page
+http://savannah.nongnu.org/projects/isarmathlib
+  Project page
+http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
+  Mail list
 
 This site is an experimental HTML rendering of fragments of the IsarMathLib
 project. IsarMathLib is a library of mathematical proofs formally verified by
@@ -82,7 +82,7 @@
 
 See:
 
- * http://formalmath.tiddlyspot.com/
+* http://formalmath.tiddlyspot.com/
 
 HOL Light
 =========
@@ -99,7 +99,7 @@
 
 See:
 
- * http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
+* http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
 
 ACL2
 ====
@@ -117,8 +117,8 @@
 
 See:
 
- * http://www.cs.utexas.edu/users/moore/acl2/
- * http://en.wikipedia.org/wiki/ACL2
+* http://www.cs.utexas.edu/users/moore/acl2/
+* http://en.wikipedia.org/wiki/ACL2
 
 PVS Specification and Verification System
 =========================================
@@ -130,9 +130,9 @@
 
 See:
 
- * http://pvs.csl.sri.com/
- * http://en.wikipedia.org/wiki/Prototype_Verification_System
- * http://www-formal.stanford.edu/clt/ARS/Entries/pvs
+* 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
 ======================================================
@@ -141,15 +141,15 @@
 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.
+* 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
@@ -160,7 +160,7 @@
 
 See:
 
- * http://www.cs.miami.edu/~tptp/
+* http://www.cs.miami.edu/~tptp/
 
 SPASS
 =====
@@ -169,15 +169,15 @@
 
 See:
 
- * http://www.spass-prover.org/index.html
+* http://www.spass-prover.org/index.html
 
 Competition
 ===========
 
 See:
 
- * http://www.cs.miami.edu/~tptp/CASC/
- * http://www.cs.albany.edu/~nvm/cade.html
+* http://www.cs.miami.edu/~tptp/CASC/
+* http://www.cs.albany.edu/~nvm/cade.html
 
 Conference
 ==========
@@ -190,16 +190,16 @@
 
 See:
 
- * http://www.ijcar.org/
- * http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning
+* http://www.ijcar.org/
+* http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning
 
 Top 100
 =======
 
-  http://www.cs.ru.nl/~freek/100/
-    (winner)
-  http://personal.stevens.edu/~nkahl/Top100Theorems.html
-    (orig list)
-  http://www.cse.unsw.edu.au/~kleing/top100/#5
-    (Isabelle)
+http://www.cs.ru.nl/~freek/100/
+  (winner)
+http://personal.stevens.edu/~nkahl/Top100Theorems.html
+  (orig list)
+http://www.cse.unsw.edu.au/~kleing/top100/#5
+  (Isabelle)