diff options
| author | B. Watson <yalhcru@gmail.com> | 2020-01-26 03:50:09 -0500 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2020-02-01 09:00:28 +0700 |
| commit | 05f829061416438cea62dd66ce4c2a0b38f3de1b (patch) | |
| tree | 5eb79e72722fb04b077b94a81697f620c486acf3 /academic | |
| parent | 0b29ed0c4adcb3daa01a207a228c8a445598b55f (diff) | |
| download | slackbuilds-05f829061416438cea62dd66ce4c2a0b38f3de1b.tar.gz | |
academic/abella: Reflow README.
Signed-off-by: B. Watson <yalhcru@gmail.com>
Diffstat (limited to 'academic')
| -rw-r--r-- | academic/abella/README | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/academic/abella/README b/academic/abella/README index aa13f891cd..a6f078794e 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. |