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