addressing comments

res/manual/src/SUMMARY.md

@@ -20,3 +20,5 @@
   - [TPTP Problem (.p)](tptp.md)
 - [Additional Help](help.md)
   - [Absolute Lemmas](lemmas.md)
+  - [Reporting Bugs](reporting.md)
+  - [Contributors](contributors.md)

res/manual/src/analyze.md

@@ -1,27 +1,20 @@
 # Analyze
 
-The `analyze` command lets users assess properties of their program through its predicate dependency graph.
+The `analyze` command lets users assess properties of their program.
+
+
+## Predicate Dependency Graph
 A predicate dependency graph for a program `Π` has all predicates occurring in `Π` as vertices, and an edge from `p` to `q` if `p` depends on `q`; that is, if `Π` contains a rule of one of the following forms
 ```
      p  :- ..., q, ...
     {p} :- ..., q, ...
 ```
-An edge `pq` is positive if `q` is not negated nor doubly negated.
+An edge `pq` is positive if `q` is neither negated nor doubly negated.
 
 
 ## Tightness
 A program is tight if its predicate dependency graph has no cycles consisting of positive edges.
-External equivalence can only be verified automatically if the program(s) are tight.
-Anthem checks this condition automatically when `verify` is invoked.
 Users can check their programs for tightness with the command
 ```
     anthem analyze program.lp --property tightness
 ```
-It may be that a non-tight program is [locally tight](https://doi.org/10.1017/S147106842300039X).
-If a user is certain that their program is locally tight, then the tightness check during verification can be bypassed by providing the flag `--bypass-tightness`.
-
-## Private Recursion
-A program contains private recursion with respect to a user guide if
-* its predicate dependency graph has a cycle such that every vertex in it is a private symbol or
-* it includes a choice rule with a private symbol in the head.
-When verifying external equivalence, any logic program is subjected to a test for private recursion and rejected if it occurs.

res/manual/src/cli.md

@@ -1,16 +1,16 @@
 # Command Line Tool
 
-Anthem is primarily a translational tool - it transforms ASP programs into theories written in the syntax of first-order logic.
+Anthem is primarily a translational tool -- it transforms ASP programs into theories written in the syntax of first-order logic.
 Additional transformations within this syntax can sometimes produce theories whose classical models coincide with the stable models of the original program.
 These transformations can be invoked via the command line using a variant of
 ```
-    translate --with <TRANSLATION>
+    anthem translate --with <TRANSLATION>
 ```
 
 Anthem can further exploit these translations from programs to equivalent (first-order) theories by invoking automated theorem provers to verify certain types of equivalence.
 Variants of the
 ```
-    verify --equivalence <EQUIVALENCE>
+    anthem verify --equivalence <EQUIVALENCE>
 ```
 command can produce problem files in the TPTP language accepted by many ATPs, or pass these problems directly to an ATP and report the results.
 
@@ -20,6 +20,7 @@ The `analyze` command lets users check whether their program(s) meet these appli
 
 For more details on these commands, and a list of available options, add the `--help` flag, e.g.
 ```
+    anthem --help
     anthem translate --help
     anthem verify --help
     anthem analyze --help

res/manual/src/contributors.md

@@ -0,0 +1,12 @@
+# Contributors
+
+We would like to thank the past and current contributors of the Anthem project!
+
+* Jorge Fandinno
+* Zach Hansen
+* Jan Heuer
+* Yuliya Lierler
+* Vladimir Lifschitz
+* Patrick Luhne
+* Torsten Schaub
+* Tobias Stolzmann

res/manual/src/guide.md

@@ -40,7 +40,7 @@ would be
 
 ### Input & Output Predicates
 
-Input and output predicates are public predicates - all other predicates are considered private to the program.
+Input and output predicates are public predicates -- all other predicates are considered private to the program.
 Input predicates are those predicates by which input data for the program are encoded.
 For example, the graph coloring program expects a set of `edge/2` and `vertex/1` facts encoding a graph and a set of colors (`color/1` facts) thus we pair that program with the user guide
 

res/manual/src/help.md

@@ -2,5 +2,3 @@
 
 Using Anthem effectively can sometimes require sophisticated proof outlines.
 This section has a couple of example lemmas that may help.
-
-To report bugs or unexpected behavior in Anthem, please email [email protected] or [email protected].

res/manual/src/outline.md

@@ -16,7 +16,7 @@ For example,
     inductive-lemma: forall N$i (N$i >= 0 -> q(N$i)).
 ```
 
-These formulas can be annotated with any direction - it is the responsibility of the programmer to ensure that the claims they formulate make sense.
+These formulas can be annotated with any direction -- it is the responsibility of the programmer to ensure that the claims they formulate make sense.
 In the example above, the universal definition of `p/1` will be used as an axiom for deriving the program from the specification, and for deriving the specification from the program.
 The inductive lemma will be proved first in both directions of the proof, and used as an axiom in subsequent steps.
 The lemma will only be used in the forward direction: first, the lemma will be derived from the specification, then the lemma and the specification will be used as axioms for deriving the program.

res/manual/src/program.md

@@ -5,7 +5,7 @@ Comments (lines prefaced by a `%`) are allowed, but directives (e.g. `#show`) ar
 
 ### The Graph Coloring Program
 
-A simple logic program without arithmetic is the following encoding of the graph coloring problem
+A simple logic program without arithmetic is the following encoding of the graph coloring problem, which can also be found in res/examples/external_equivalence/coloring/coloring.lp.
 
 ```
     {color(X,Z)} :- vertex(X), color(Z).
@@ -19,17 +19,19 @@ A simple logic program without arithmetic is the following encoding of the graph
 
 ### The Primes Programs
 
-A challenging task for Anthem is verifying the external equivalence of the following logic program, `primes.1`
+A challenging task for Anthem is verifying the external equivalence of the following logic program, `primes.1.lp`
 
 ```
     composite(I*J) :- I > 1, J > 1.
     prime(I) :- I = a..b, not composite(I).
 ```
 
-to the program `primes.2`
+to the program `primes.2.lp`
 
 ```
     sqrtb(M) :- M = 1..b, M * M <= b, (M+1)*(M+1) > b.
     composite(I*J) :- sqrtb(M), I = 2..M, J = 2..b.
     prime(I) :- I = a..b, not composite(I).
 ```
+
+This example can be found in the res/examples/external_equivalence/primes/simple directory.

res/manual/src/reporting.md

@@ -0,0 +1,5 @@
+# Reporting Bugs
+
+To report bugs or unexpected behavior in Anthem, please email either
+ * <[email protected]>
+ * <[email protected]>

res/manual/src/tptp.md

@@ -107,4 +107,4 @@ For example, for a problem containing an integer placeholder `k$`, symbolic cons
 Since strong equivalence does not support user guides or placeholders, the standard preamble is extended with \\(F \cup O \cup R\\) instead.
 Additionally, we need axioms representing the ordering between the `here` and `there` worlds.
 Thus, for a pair of predicates `(hp, tp)` we add the axiom
-\\[hp \rightarrow tp\\]
+\\[\widetilde{\forall} (hp \rightarrow tp) \\]

res/manual/src/translate.md

@@ -12,7 +12,7 @@ A mini-gringo program consists of three types of rules: choice, basic, and const
         :- B1, ..., Bn.
 ```
 
-where H is an atom and each Bi is a singly, doubly, or non-negated atom or comparison.
+where `H` is an atom and each `Bi` is a singly, doubly, or non-negated atom or comparison.
 
 
 ## The Target Language
@@ -100,3 +100,4 @@ Access the `completion` transformation via the `translate` command, e.g.
     anthem translate program.lp --with tau-star,completion
 ``` -->
 However, keep in mind that the original program must be tight for the models of the completion to coincide with the stable models of the program!
+This property is not checked automatically during translation.

res/manual/src/verify.md

@@ -1,8 +1,8 @@
 # Verification
 The `verify` command uses the ATP [vampire](https://vprover.github.io/) to automatically verify that some form of equivalence holds between two programs, or between a program and a target language specification.
 These equivalence types are described below.
-By default, Anthem verifies equivalence - this can also be specified by adding the `--direction universal` flag.
-To verify one implication of the equivalence (e.g. `->`) add the `--direction forward` flag (conversely, the `--direction backward` flag for `<-`).
+By default, Anthem verifies equivalence -- this can also be specified by adding the `--direction universal` flag.
+To verify one implication of the equivalence (e.g. \\(\rightarrow\\)) add the `--direction forward` flag (conversely, the `--direction backward` flag for \\(\leftarrow\\)).
 
 
 ## Strong Equivalence
@@ -35,7 +35,7 @@ paired with the user guide
     input: n -> integer.
     output: prime/1.
 ```
-This user guide indicates that `n` is a placeholder - that is, `n` is a symbolic constant that may be treated in a non-Herbrand way.
+This user guide indicates that `n` is a placeholder -- that is, `n` is a symbolic constant that may be treated in a non-Herbrand way.
 Specifically, `n` is to be interpreted as an integer.
 The second line of the user guide declares that the external behavior of these programs is defined by the extent of the `prime/1` predicate.
 If these extents coincide for all interpretations that interpret `n` as an integer, then we consider the programs externally equivalent.
@@ -51,12 +51,24 @@ Note that the `universal` direction is the default, and may be dropped.
 To verify that the program posesses a certain property expressed by the specification, set the direction to backward (`--direction backward`).
 To verify that the program's external behavior is a consequence of the specification, set the direction to forward (`--direction forward`).
 
-##### Renaming Private Predicates
+#### Tightness and Private Recursion
+External equivalence can only be verified automatically if the program(s) are tight.
+Anthem checks this condition by default when `verify` is invoked.
+It may be that a non-tight program is [locally tight](https://doi.org/10.1017/S147106842300039X).
+If a user is certain that their program is locally tight, then the tightness check can be bypassed by providing the flag `--bypass-tightness`.
+
+A program contains private recursion with respect to a user guide if
+* its predicate dependency graph has a cycle such that every vertex in it is a private symbol or
+* it includes a choice rule with a private symbol in the head.
+During external equivalence verification, any logic program is subjected to a test for private recursion and rejected if it occurs.
+This step cannot be bypassed.
+
+#### Renaming Private Predicates
 In the example above, `prime/1` is a public predicate, and both definitions of `composite/1` are private predicates.
 The predicates named `composite/1` are two different predicates, but they have conflicting names.
 In such a case, the conflicting predicate from the program is renamed with an `_p`, e.g. `composite_p/1`.
 
-##### Replacing Placeholders
+#### Replacing Placeholders
 Syntactically, `n` is a symbolic constant, but it has been paired with a user guide specifying that it should be interpreted as an integer.
 However, the standard interpretations of interest interpret symbolic constants and numerals as themselves.
 Thus, in an external equivalence verification task, we replace every occurrence of a symbolic constant `n` with an integer-sorted function constant named `n`, e.g. `n$i`.
@@ -118,7 +130,7 @@ into a pair of conjectures
 \\[\forall X F(X) \rightarrow G(X), \forall X G(X) \rightarrow F(X)\\]
 which are passed to `vampire` separately.
 
-Anthem can parallelize at the problem level with the `--prover-instances` (`-n`) argument - this determines how many instances of the backend ATP are invoked.
+Anthem can parallelize at the problem level with the `--prover-instances` (`-n`) argument -- this determines how many instances of the backend ATP are invoked.
 It can also pass parallelism arguments to the ATP.
 `--prover-cores` (`-m`) determines how many threads each ATP instance can use.
-The `--time-limt` flag (`-t`) is the time limit in seconds to prove each problem passed to an ATP.
+The `--time-limit` flag (`-t`) is the time limit in seconds to prove each problem passed to an ATP.