updates

res/manual/src/analyze.md

@@ -17,7 +17,7 @@ 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 (see ???).
+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

res/manual/src/verify.md

@@ -1,13 +1,13 @@
 # Verification
-The `verify` command uses the ATP `vampire` to automatically verify that some form of equivalence holds between two programs, or between a program and a target language specification.
+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 `<-`).
 
 
 ## Strong Equivalence
 Strong equivalence is a property that holds for a pair of programs (`Π1`, `Π2`) if `Π1 U Π` has the same answer sets as `Π2 U Π`, for any program `Π`.
-This property can be verified for mini-gringo programs by determining the equivalence of `τ*Π1` and `τ*Π2` within the HTA (here-and-there with arithmetic) deductive system.
+This property can be verified for mini-gringo programs by determining the equivalence of `τ*Π1` and `τ*Π2` within the [HTA](https://doi.org/10.1017/S1471068421000338) (here-and-there with arithmetic) deductive system.
 This problem can be reduced to a first-order reasoning task by applying the gamma transformation, e.g. determining the equivalence of `γτ*Π1` and `γτ*Π2`.
 The property can be automatically verified with the command
 ```
@@ -18,8 +18,7 @@ The property can be automatically verified with the command
 ## External Equivalence
 Strong equivalence is sometimes too strong of a condition.
 Sometimes we are interested in the behavior of only certain program predicates when the program is paired with a user guide defining the context in which the program should be used.
-This is referred to as "external behavior."
-A precise definition of external behavior equivalence can be found in ???
+This is referred to as [external behavior](https://doi.org/10.1017/S1471068423000200).
 
 As an example, consider the programs
 ```
@@ -46,6 +45,7 @@ Anthem can verify this claim automatically with the command
     anthem verify --equivalence external <SPECIFICATION> <PROGRAM> <USER GUIDE> --direction universal
 ```
 This amounts to confirming that the program implements the specification under the assumptions of the user guide.
+This is done by transforming the program(s) into their formula representations using the `τ*` and `COMP` transformations, then deriving their equivalence.
 
 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`).
@@ -57,17 +57,22 @@ The predicates named `composite/1` are two different predicates, but they have c
 In such a case, the conflicting predicate from the program is renamed with an `_p`, e.g. `composite_p/1`.
 
 ##### Replacing Placeholders
-Syntactically, `n` is a symbolic constant, but it has been paired with a user specifying that it should be interpreted as an integer.
+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
+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`.
+This applies to all files involved: programs, specifications, user guides, and proof outlines.
+Thus, while running the example above, you could expect to see such output as
+```
+tbd
+```
 
 
 ### Answer Set Equivalence
 Answer set equivalence (which asserts two programs have the same answer sets) is a special case of external equivalence.
 A user guide without placeholders, assumptions or input declarations, that contains every predicate in a pair of programs `(Π1, Π2)` as an output declaration, can be used to validate the answer set equivalence of `Π1` and `Π2`.
 
 ## Interpreting Anthem Output
-Anthem will pass a series of problems to an ATP backend and report the status of each using the SZS status ontology.
+Anthem will pass a series of problems to an ATP backend and report the status of each using the [SZS status ontology](https://dblp.org/rec/conf/lpar/Sutcliffe08.bib).
 If all problems are successfully verified, Anthem will report
 ```
     Success!
@@ -86,3 +91,15 @@ Note that this is NOT a proof that the equivalence property does not hold.
 Rather than invoking `vampire`, Anthem can produce a set of TPTP problem files that can be passed manually to a variety of ATPs.
 If each problem is verified (the ATP reports a `Theorem` SZS status), then the verification can be considered successfully verified.
 To invoke this option, add the `--no-proof-search` flag to a verification command, along with `--save-problems <DIR>` to save problem files to a directory of choice.
+
+
+## Additional Options
+
+Adding a `--no-simplify` flag disables the HT-equivalent simplifications that are automatically applied to the theory `COMP[τ*Π]`.
+
+Adding a `--no-eq-break` flag disables "equivalence breaking."
+When equivalence breaking is enabled, Anthem turns every conjecture of the form
+\\[\forall X F(X) \leftrightarrow G(X)\\]
+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.