aboutsummaryrefslogtreecommitdiff
path: root/academic
diff options
context:
space:
mode:
authorB. Watson <yalhcru@gmail.com>2020-01-26 03:50:09 -0500
committerWilly Sudiarto Raharjo <willysr@slackbuilds.org>2020-02-01 09:00:28 +0700
commit05f829061416438cea62dd66ce4c2a0b38f3de1b (patch)
tree5eb79e72722fb04b077b94a81697f620c486acf3 /academic
parent0b29ed0c4adcb3daa01a207a228c8a445598b55f (diff)
academic/abella: Reflow README.
Signed-off-by: B. Watson <yalhcru@gmail.com>
Diffstat (limited to 'academic')
-rw-r--r--academic/abella/README29
1 files changed, 17 insertions, 12 deletions
diff --git a/academic/abella/README b/academic/abella/README
index aa13f891cdcc6..a6f078794eaab 100644
--- a/academic/abella/README
+++ b/academic/abella/README
@@ -1,7 +1,9 @@
-Abella is an interactive theorem prover based on lambda-tree syntax.
-This means that Abella is well-suited for reasoning about the meta-theory of programming languages
-and other logical systems which manipulate objects with binding. For example, the following applications
-are included in the distribution of Abella.
+Abella is an interactive theorem prover based on lambda-tree syntax.
+
+This means that Abella is well-suited for reasoning about the meta-theory
+of programming languages and other logical systems which manipulate
+objects with binding. For example, the following applications are included
+in the distribution of Abella.
* Various results on the lambda calculus involving big-step evaluation, small-step evaluation, and typing judgments
* Cut-admissibility for a sequent calculus
@@ -15,11 +17,14 @@ are included in the distribution of Abella.
For Full List:
http://abella-prover.org/examples/index.html
-Abella uses a two-level logic approach to reasoning.
-Specifications are made in the logic of second-order hereditary Harrop formulas using lambda-tree syntax.
-This logic is executable and is a subset of the AProlog language
-(see the Teyjus system for an implementation of this language).
-The reasoning logic of Abella is the culmination of a series of extensions to proof theory for the
-treatment of definitions, lambda-tree syntax, and generic judgments.
-The reasoning logic of Abella is able to encode the semantics of our specification logic as a
-definition and thereby reason over specifications in that logic.
+Abella uses a two-level logic approach to reasoning. Specifications
+are made in the logic of second-order hereditary Harrop formulas using
+lambda-tree syntax. This logic is executable and is a subset of the
+AProlog language (see the Teyjus system for an implementation of this
+language).
+
+The reasoning logic of Abella is the culmination of a series of extensions
+to proof theory for the treatment of definitions, lambda-tree syntax,
+and generic judgments. The reasoning logic of Abella is able to encode
+the semantics of our specification logic as a definition and thereby
+reason over specifications in that logic.