Merge branch 'master' into zach/placeholders3

README.md

@@ -1,3 +1,16 @@
 # anthem
 
-A translator between answer set programs and first-order logic
+`anthem` is a command line application for translating answer set programs in the mini-gringo dialect of [clingo](https://potassco.org/clingo/) to first-order theories.
+Using an automated theorem prover, these theories can then be used to verify properties of the original programs, such as strong and external equivalence.
+
+Check out the [Manual](https://potassco.org/anthem/) to learn how to install and use `anthem`.
+
+If you want to use `anthem` as a library to build your own application, you can do so.
+Check out the [API documentation](https://docs.rs/anthem/) for the available functionalities.
+
+## License
+
+`anthem` is distributed under the terms of the MIT license.
+See [LICENSE](LICENSE) for details!
+
+Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in `anthem` by you shall be licensed as above, without any additional terms or conditions.

res/examples/external_equivalence/coloring/README.md

@@ -2,6 +2,5 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence external --out-dir out coloring.spec coloring.lp coloring.ug
+anthem verify --equivalence external coloring.spec coloring.lp coloring.ug
 ```

res/examples/external_equivalence/cover/README.md

@@ -4,15 +4,13 @@
 To run the original program-to-specification verification task, use
 
 ```
-mkdir -p out/p2s
-anthem verify --equivalence=external --out-dir out/p2s cover.spec cover.lp cover.ug
+anthem verify --equivalence external cover.spec cover.lp cover.ug
 ```
 
 To run the program-to-program verification task against a new program with a symmetry breaking constraint, use
 
 ```
-mkdir -p out/p2p
-anthem verify --equivalence=external --out-dir out/p2p cover.lp cover_sym_break.lp cover.ug
+anthem verify --equivalence external cover.lp cover_sym_break.lp cover.ug
 ```
 
 ## Origin

res/examples/external_equivalence/primes/complex/README.md

@@ -2,11 +2,8 @@
 
 ## Usage
 ```
-mkdir -p out/safe
-anthem verify --equivalence=external --out-dir out/safe primes.1.lp primes.2.lp primes.ug
-
-mkdir -p out/optimized
-anthem verify --equivalence=external --out-dir out/optimized primes.2.lp primes.3.lp primes.ug
+anthem verify --equivalence=external primes.1.lp primes.2.lp primes.ug
+anthem verify --equivalence=external primes.2.lp primes.3.lp primes.ug
 ```
 
 ## Origin

res/examples/external_equivalence/primes/simple/README.md

@@ -2,6 +2,5 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=external --out-dir out primes.1.lp primes.2.lp primes.ug primes.po
+anthem verify --equivalence external primes.1.lp primes.2.lp primes.ug primes.po
 ```

res/examples/external_equivalence/trivial/first_order/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=external --out-dir out first_order.spec first_order.lp first_order.ug
+anthem verify --equivalence external first_order.spec first_order.lp first_order.ug
 ```
 
 ## Origin

res/examples/external_equivalence/trivial/propositional/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=external --out-dir out propositional.spec propositional.lp propositional.ug
+anthem verify --equivalence external propositional.spec propositional.lp propositional.ug
 ```
 
 ## Origin

res/examples/strong_equivalence/bounds/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=strong --out-dir out bounds.1.lp bounds.2.lp
+anthem verify --equivalence strong bounds.1.lp bounds.2.lp
 ```
 
 ## Origin

res/examples/strong_equivalence/choice/README.md

@@ -3,7 +3,7 @@
 ## Usage
 ```
 mkdir out
-anthem verify --equivalence=strong --out-dir out choice.1.lp choice.2.lp
+anthem verify --equivalence strong choice.1.lp choice.2.lp
 ```
 
 ## Origin

res/examples/strong_equivalence/successor/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=strong --out-dir out successor.1.lp successor.2.lp
+anthem verify --equivalence strong successor.1.lp successor.2.lp
 ```
 
 ## Origin

res/examples/strong_equivalence/transitive/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=strong --out-dir out transitive.1.lp transitive.2.lp
+anthem verify --equivalence strong transitive.1.lp transitive.2.lp
 ```
 
 ## Origin

res/examples/strong_equivalence/trivial/README.md

@@ -2,8 +2,7 @@
 
 ## Usage
 ```
-mkdir out
-anthem verify --equivalence=strong --out-dir out trivial.1.lp trivial.2.lp
+anthem verify --equivalence=strong trivial.1.lp trivial.2.lp
 ```
 
 ## Origin

res/manual/src/SUMMARY.md

@@ -7,14 +7,14 @@
 - [Quick Start]()
 
 # Reference Guide
-- [Command Line Tool]()
+- [Command Line Tool](cli.md)
   - [translate]()
   - [verify]()
   - [analyze]()
-- [Input File Format]()
-  - [Program (.lp)]()
+- [Input File Format](input_files.md)
+  - [Program (.lp)](program.md)
   - [Specification (.spec)]()
-  - [User Guide (.ug)]()
-  - [Proof Outline (.po)]()
+  - [User Guide (.ug)](guide.md)
+  - [Proof Outline (.po)](outline.md)
 - [Output File Format]()
   - [TPTP Problem (.p)]()

res/manual/src/cli.md

@@ -0,0 +1,5 @@
+# Command Line Tool
+
+### The mini-GRINGO Dialect
+
+### The Target Language

res/manual/src/guide.md

@@ -0,0 +1,43 @@
+# User Guide (.ug)
+
+A user guide contains input declarations, output declarations, and annotated formulas with the assumption role. An input declaration is a predicate or a placeholder. For example, the following are valid input declarations.
+
+* input: p/0.
+* input: edge/2.
+* input: a.
+* input: n -> integer.
+
+Collectively, these lines denote that `p/0` and `edge/2` are input predicates, that `a` is an object-sorted placeholder, and that `n` is an integer-sorted placeholder. Anthem will throw an error if two placeholders with the same name are declared with different sorts.
+
+### Placeholders
+
+Syntactically, a placeholder is a symbolic constant. When an io-program `P` containing a symbolic constant `n` is paired with a user guide specifying `n` as a placeholder, every occurrence of `n` within `P` will be replaced by a zero-arity function constant of the specified sort. In the example above, `a` will be replaced by `a$g`, and `n` will be replaced by `n$i`. Placeholders are replaced in a similar fashion within specifications, proof outlines, and user guide assumptions. For example, within the context of a user guide containing the declaration
+
+* input: n -> integer.
+
+the (simplified) formula representation of the following rule
+
+* p(X) :- X = 1..n.
+
+would be
+
+* forall (X) ( p(X) <-> exists I$i (1 <= I$i <= n$i and X = I$i) ).
+
+### Input & Output Predicates
+
+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
+
+* input: vertex/1.
+* input: edge/2.
+* input: color/1.
+* output: color/2.
+
+Output predicates function similarly to the `#show` directive in CLINGO. The extent of the output predicates define the external behavior of a program. In the graph coloring example, the external behavior is defined by the `color/2` predicate (mapping vertices to colors). Conversely, `aux/1` is the only private predicate.
+
+### Assumptions
+
+The only type of annotated formula accepted by user guides are assumptions. These assumptions are intended to define an acceptable class of inputs. Thus, they should not contain output symbols (this will trigger an error).
+
+### 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 `(P1, P2)` as an output declaration, can be used to validate the answer set equivalence of `P1` and `P2`.

res/manual/src/input_files.md

@@ -0,0 +1,14 @@
+# Input File Format
+
+### Annotated Formulas
+Specifications, user guides, and proof outlines contain annotated formulas.
+
+An annotated formula is a first-order formula from the target language annotated with a role, and (optionally) with a name and/or direction. In general, an annotated formula is written
+
+role(direction)[name]: formula.
+
+Valid roles are assumption, spec, definition, lemma, inductive-lemma.
+
+Valid directions are forward, backward, universal.
+
+Names are alphanumeric strings.

res/manual/src/outline.md

@@ -0,0 +1,68 @@
+# Proof Outline (.po)
+
+A proof outline is understood as a sequence of steps for Anthem to take while attempting to construct a proof. When a step is verified successfully, the associated formula will be used as an axiom while attempting to prove subsequent steps. Typically, a proof outline is used to extend the set of axioms used within an (external equivalence) verification task.
+
+
+Proof outlines consist of annotated formulas of three types:
+
+1. definitions,
+2. lemmas,
+3. inductive lemmas.
+
+For example,
+
+* definition(universal)[completed_def_of_p]: forall X (p(X) <-> q(X) and not X = 0).
+* lemma(forward)[int_q]: exists N$i q(N$i).
+* 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. 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.
+
+### Lemmas
+Lemmas have a general form
+
+* lemma(direction)[name]: F.
+
+where F is a target language formula. Within lemmas a formula F with free variables is interpreted as the universal closure of F.
+
+### Inductive Lemmas
+Inductive lemmas have a general form
+
+* inductive-lemma(direction)[name]: forall X N ( N >= n -> F(X,N) ).
+
+where n is an integer, X is a tuple of variables, N is an integer variable and F is a target language formula. As with lemmas, a formula with free variables is understood as an abbreviation for the universal closure of said formula.
+
+Within a proof outline, an inductive lemma is interpreted as an instruction to prove two conjectures:
+
+1. forall X ( F(X,n) )
+2. forall X N ( N >= n and F(X,N) -> F(X,N+1) )
+
+If both the first (the base case) and the second (the inductive step) conjectures are proven, then the original formula is treated as an axiom in the remaining proof steps.
+
+### Definitions
+Definitions are treated similarly to assumptions - they are assumed to define the extent of a new predicate introduced for convenience within a proof outline. They have the general form
+
+* definition(direction)[name]: forall X ( p(X) <-> F(X) ).
+
+where
+
+1. X is a tuple of distinct integer or general variables
+2. p is a totally fresh predicate symbol (it doesn’t occur outside of the proof outline)
+3. F is a target language formula with free variables X that doesn’t contain atoms whose predicate symbol is p.
+
+A sequence of definitions is valid if any definitions p used within each F were defined previously in the sequence. Intuitively, a definition should not depend on definitions that have not yet been defined. Thus, substituting the RHS for the LHS is always possible, and we could expand the body of the last definition by replacing any occurrences of previously defined definitions with their corresponding RHS.
+
+Anthem will produce warnings about the following cases:
+
+1. A definition where the defined predicate contains a variable that does not occur in the RHS is likely a mistake.
+2. A lemma referencing a definition that hasn’t yet been defined in the proof outline is poor style.
+
+
+### A Complete Example
+
+The external equivalence of the Primes Programs can be verified with the assistance of the following proof outline:
+
+* definition: forall I$ N$ (sqrt(I$,N$) <-> I$ >= 0 and I$ * I$ < N$ <= (I$+1) * (I$+1) ).
+* lemma: sqrt(I$,N$) and (I$+1) * (I$+1) <= N$+1 -> sqrt(I$+1,N$+1).
+* inductive-lemma: N$ >= 0 -> exists I$ sqrt(I$,N$).
+* lemma: b$i >= 1 -> (sqrtb(I$) <-> sqrt(I$, b$i)).
+* lemma: I$ >= 0 and J$ >= 0 and I$*J$ <= b and sqrtb(N$) -> I$ <= N$ or J$ <= N$.

res/manual/src/program.md

@@ -0,0 +1,27 @@
+# Program (.lp)
+
+
+### The Graph Coloring Program
+
+A simple logic program without arithmetic is the following encoding of the graph coloring program
+
+* {color(X,Z)} :- vertex(X), color(Z).
+* :- color(X,Z1), color(X,Z2), Z1 != Z2.
+* aux(X) :- vertex(X), color(Z), color(X,Z).
+* :- vertex(X), not aux(X).
+* :- edge(X,Y), color(X,Z), color(Y,Z).
+
+
+
+### The Primes Programs
+
+A challenging task for Anthem is verifying the external equivalence of the following logic program, `primes.1`
+
+* composite(I*J) :- I > 1, J > 1.
+* prime(I) :- I = a..b, not composite(I).
+
+to the program `primes.2`
+
+* 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).