Introduction

Command Line Tool

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

    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

    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.

The automated verification of external equivalence is only applicable to certain mini-gringo programs. The analyze command lets users check whether their program(s) meet these applicability requirements. (Note that this is done automatically when the verify command is used).

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

Translation

The mini-gringo Dialect

The mini-gringo dialect is a subset of the language supported by the answer set solver clingo. It has been extensively studied within the ASP literature as a theoretical language whose semantics can be formally defined via transformations into first-order theories interpreted under the semantics of here-and-there (with arithmetic).

A mini-gringo program consists of three types of rules: choice, basic, and constraint:

    {H} :- B1, ..., Bn.
     H  :- B1, ..., Bn.
        :- B1, ..., Bn.

where H is an atom and each Bi is a singly, doubly, or non-negated atom or comparison.

The Target Language

The formula representation language (often called the “target” of ASP-to-FOL transformations) is a many-sorted first-order language. Specifically, all terms occurring in a mini-gringo program belong to the language’s supersort, general (abbreviated g). It contains two special terms, #inf and #sup, representing the minimum and maximum elements in the total order on general terms. Numerals (which have a one-to-one correspondence with integers) are a subsort of this sort, they belong to a sort referred to as integer (abbreviated i). All other general terms are symbolic constants, they belong to the symbol sort (abbreviated s).

Variables ranging over these sorts are written as name$sort, where name is a capital word and sort is one of the sorts defined above. Certain abbreviations are permitted; the following are examples of valid variables:

    V$general, V$g, V
    X$integer, X$i, X$
    Var$symbol, Var$s

These lines represent equivalent ways of writing a general variable named V, an integer variable named X, and a symbol variable named Var.

The Formula Representation Transformation (tau*)

The transformation referred to in the literature as tau* (τ*) is a collection of transformations from mini-gringo programs into the syntax of first-order logic, taking special consideration for the fact that while an ASP term can have 0, 1, or many values, a first-order term can have only one. In the presence of arithmetic terms or intervals, such as 1/0 or 0..9, this introduces translational complexities. Interested readers should refer here for details.

The tau* transformation is fundamental to Anthem. For a mini-gringo program Π, the HTA (here-and-there with arithmetic) models of the formula representation τ*Π correspond to the stable models of Π. Furthermore, additional transformations can, in certain cases, produce formula representations within the same language whose classical models capture the behavior of Π.

Access the τ* transformation via the translate command, e.g.

    anthem translate program.lp --with tau-star

Transformations Within the Target Language

The following transformations translate theories (typically) obtained from applying the τ* transformation to a mini-gringo program Π into theories whose classical models coincide with the stable models of Π.

Gamma

The gamma (γ) transformation (introduced by Pearce for propositional programs) and extended to first-order programs in Heuer’s Procedure was implemented in an unpublished Anthem prototype. The implementation of this system follows the description found here. For a predicate p, a new predicate representing satisfaction in the “here” world named hp is introduced. Similarly, predicate tp represents satisfaction of p in the “there” world. Thus, for a theory

    forall X ( exists I$ (X = I$ and 3 < I$ < 5) -> p(X) ).

gamma produces

    forall X ((exists I$i (X = I$i and 3 < I$i < 5) -> hp(X)) and (exists I$i (X = I$i and 3 < I$i < 5) -> tp(X))).

Access the gamma transformation via the translate command, e.g.

    anthem translate theory.spec --with gamma

Completion

This is an implementation of an extension of Clark’s Completion. It accepts a completable theory (such as those produced by τ*) and produces the (first-order) completion. For example, the completion of the theory

    forall X ( X = 1 -> p(X) ).
    forall X Y ( q(X,Y) -> p(X) ).

    forall X ( p(X) <-> X = 1 or exists Y q(X,Y) ).

Access the completion transformation via the translate command, e.g.

    anthem translate theory.spec --with 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.

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. 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. $\rightarrow$) add the --direction forward flag (conversely, the --direction backward flag for $\leftarrow$).

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 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

    anthem verify --equivalence strong p1.lp p2.lp

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.

As an example, consider the programs

    composite(I*J) :- I > 1, J > 1.
    prime(I) :- I = 2..n, not composite(I).

and

    composite(I*J) :- I = 2..n, J = 2..n.
    prime(I) :- I = 2..n, not composite(I).

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. 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.

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). To verify that the program’s external behavior is a consequence of the specification, set the direction to forward (--direction forward).

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. 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

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. 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

> Proving forward_problem_0...
Axioms:
    forall V1 (composite(V1) <-> exists I J (exists I1$i J1$i (V1 = I1$i * J1$i and I1$i = I and J1$i = J) and (exists Z Z1 (Z = I and Z1 = 1 and Z > Z1) and exists Z Z1 (Z = J and Z1 = 1 and Z > Z1))))
    forall V1 (composite_p(V1) <-> exists I J (exists I1$i J1$i (V1 = I1$i * J1$i and I1$i = I and J1$i = J) and (exists Z Z1 (Z = I and exists I$i J$i K$i (I$i = 2 and J$i = n$i and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1) and exists Z Z1 (Z = J and exists I$i J$i K$i (I$i = 2 and J$i = n$i and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1))))
    forall V1 (prime(V1) <-> exists I (V1 = I and (exists Z Z1 (Z = I and exists I$i J$i K$i (I$i = 2 and J$i = n$i and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1) and exists Z (Z = I and not composite(Z)))))

Conjectures:
    forall V1 (prime(V1) -> exists I (V1 = I and (exists Z Z1 (Z = I and exists I$i J$i K$i (I$i = 2 and J$i = n$i and Z1 = K$i and I$i <= K$i <= J$i) and Z = Z1) and exists Z (Z = I and not composite_p(Z)))))
> Status:
    Theorem

for each problem. The (problem name, axioms, conjecture) triple is printed as soon as the ATP is invoked, and the status (indicating if the ATP proved the conjecture from the axioms successfully) is printed once the ATP invocation returns. If all the problems are proven (Theorem status) then Anthem reports success on the verification task.

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. If all problems are successfully verified, Anthem will report

    Success!

which indicates that the equivalence property holds.

Otherwise, Anthem will report

    Failure!

indicating that the equivalence property could not be verified. Note that this is NOT a proof that the equivalence property does not hold.

Problem Files vs End-to-end Use

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.

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-limit flag (-t) is the time limit in seconds to prove each problem passed to an ATP.

Analyze

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 neither negated nor doubly negated.

Tightness

A program is tight if its predicate dependency graph has no cycles consisting of positive edges. Users can check their programs for tightness with the command

    anthem analyze program.lp --property tightness

Input File Format

Writing Target Language Formulas

Terms are symbolic constants (a, aB, etc.), numerals (1, -50, etc.), variables (V, Var$i, etc.), zero-arity function constants (a$g, n$i, etc.), or #inf or #sup. Terms composed of arithmetic operations +, -, * and integer-sorted operands are supported (1 + 3, X$ - Y$, etc.). Atoms are predicate symbols followed by a tuple of terms (p(1, X, V$), q, etc.). Comparisons consist of a general term followed by one or more (relation, term) pairs (a = b, 0 <= N$ < 9, etc.). The relations

    =, !=, <, >, <=, =>

are supported. The traditional binary connectives conjunction, disjunction, negation, implication, and equivalence are supported (written and, or, not, -> and <->, respectively). The reverse implication connective is defined as follows:

    F <- G

is understood as

    G -> F

The universal and existential quantifiers are written forall and exists. Variables following a quantifier are separated by whitespace. For example,

    forall X Y ( p(X, Y) <-> exists Z ( q(X,Y,Z) and X != Z) )

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. In the task of proving the equivalence of a program Π to a specification S, we must derive

Π from S (the forward direction)
S from Π (the backward direction)

Thus, a formula annotated with the universal direction will be used in both directions. Finally, names are alphanumeric strings. Omitting a direction defaults to universal, whereas omitting a name defaults to unnamed_formula.

Program (.lp)

A logic program Π must be written in the mini-gringo dialect. It should not have any rule heads containing input symbols. Comments (lines prefaced by a %) are allowed, but directives (e.g. #show) are not.

The Graph Coloring Program

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).
    :- 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.lp

    composite(I*J) :- I > 1, J > 1.
    prime(I) :- I = a..b, not composite(I).

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.

Specification (.spec)

The verification of external equivalence compares a mini-gringo program to a specification. A specification can be written as another mini-gringo program Π or as a control language specification S.

Logic Program Specifications

If the specification is a program Π, then Π must not contain input symbols in any rule heads. Additionally, Π must be tight and free of private recursion. This is because the formula representation of Π will be obtained via tau-star and completion (COMP[τ*Π1]). The completed definitions of private predicates from this theory will be treated as assumptions in the forward and backward directions of the proof. The remaining formulas from COMP[τ*Π1] will be treated analogously to formulas with the spec(universal) annotation (as described below).

Control Language Specifications

If the specification is S, it consists of annotated formulas of two types: assumptions and specs. Both types of formulas must be closed. Furthermore, atoms within assumptions should only have input predicate symbols. The following is a specification defining the expected behavior of the Graph Coloring program:

    assumption: forall X Y (edge(X,Y) -> vertex(X) and vertex(Y)).
    spec: forall X Z (color(X,Z) -> vertex(X) and color(Z)).
    spec: forall X (vertex(X) -> exists Z color(X,Z)).
    spec: forall X Z1 Z2 (color(X,Z1) and color(X,Z2) -> Z1 = Z2).
    spec: not exists X Y Z (edge(X,Y) and color(X,Z) and color(Y,Z)).

Specs with the universal annotation are treated as axioms in the forward direction of the proof, and as conjectures in the backward direction. A spec with a forward annotation is an axiom in the forward direction and ignored in the backward direction. Similarly, a spec with a backward annotation is a conjecture in the backward direction and ignored in the forward direction.

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 Π containing a symbolic constant n is paired with a user guide specifying n as a placeholder, every occurrence of n within Π 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).

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:

definitions,
lemmas,
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:

forall X ( F(X,n) )
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

X is a tuple of distinct integer or general variables
p is a totally fresh predicate symbol (it doesn’t occur outside of the proof outline)
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:

A definition where the defined predicate contains a variable that does not occur in the RHS is likely a mistake.
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$.

Output File Format

Variants of the --verify command can produce problem files that can be passed to an ATP. For example, the command

anthem verify --equivalence external res/examples/external_equivalence/primes/simple/primes.{1.lp,2.lp,ug} --no-proof-search --save-problems ./

produces a set of TPTP problems files in the current directory (./) without invoking an ATP to verify them. In this case, verifying each problem file amounts to proving the external equivalence of the programs primes.1.lp and primes.2.lp under the assumptions of primes.ug.

TPTP Problem (.p)

Anthem produces TPTP problem files containing typed first-order formulas (TFF).

The Standard Preamble

The standard preamble (standard_interpretations.p) contains (problem-independent) types and axioms partially axiomatizing the conditions of standard interpretations.

Types

The type declarations define the sorts of the target (formula representation) language (the numeral type corresponds to vampire’s built-in integer type, $int):

    tff(type, type, general: $tType).
    tff(type, type, symbol: $tType).

Objects within the universe of a subsort must be mapped to an object within the supersort universe:

    tff(type, type, f__integer__: ($int) > general).
    tff(type, type, f__symbolic__: (symbol) > general).
    tff(type, type, p__is_integer__: (general) > $o).
    tff(type, type, p__is_symbolic__: (general) > $o).

#inf and #sup are special general terms which do not belong to the symbol or numeral subsorts:

    tff(type, type, c__infimum__: general).
    tff(type, type, c__supremum__: general).

General terms are ordered:

    tff(type, type, p__less_equal__: (general * general) > $o).
    tff(type, type, p__less__: (general * general) > $o).
    tff(type, type, p__greater_equal__: (general * general) > $o).
    tff(type, type, p__greater__: (general * general) > $o).

Axioms

    tff(axiom, axiom, ![X: general]: (p__is_integer__(X) <=> (?[N: $int]: (X = f__integer__(N))))).
    tff(axiom, axiom, ![X1: general]: (p__is_symbolic__(X1) <=> (?[X2: symbol]: (X1 = f__symbolic__(X2))))).

The universe of general terms consists of symbols, numerals, #inf, and #sup:

    tff(axiom, axiom, ![X: general]: ((X = c__infimum__) | p__is_integer__(X) | p__is_symbolic__(X) | (X = c__supremum__))).

The mappings from subsorts to supersorts should preserve equality between terms:

    tff(axiom, axiom, ![N1: $int, N2: $int]: ((f__integer__(N1) = f__integer__(N2)) <=> (N1 = N2))).
    tff(axiom, axiom, ![S1: symbol, S2: symbol]: ((f__symbolic__(S1) = f__symbolic__(S2)) <=> (S1 = S2))).

Numerals are ordered analogously to integers:

    tff(axiom, axiom, ![N1: $int, N2: $int]: (p__less_equal__(f__integer__(N1), f__integer__(N2)) <=> $lesseq(N1, N2))).

The ordering is transitive:

    tff(axiom, axiom, ![X1: general, X2: general, X3: general]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X3)) => p__less_equal__(X1, X3))).

The ordering is total:

    tff(axiom, axiom, ![X1: general, X2: general]: ((p__less_equal__(X1, X2) & p__less_equal__(X2, X1)) => (X1 = X2))).
    tff(axiom, axiom, ![X1: general, X2: general]: (p__less_equal__(X1, X2) | p__less_equal__(X2, X1))).

The remaining relations are defined in terms of less or equal:

    tff(axiom, axiom, ![X1: general, X2: general]: (p__less__(X1, X2) <=> (p__less_equal__(X1, X2) & (X1 != X2)))).
    tff(axiom, axiom, ![X1: general, X2: general]: (p__greater_equal__(X1, X2) <=> p__less_equal__(X2, X1))).
    tff(axiom, axiom, ![X1: general, X2: general]: (p__greater__(X1, X2) <=> (p__less_equal__(X2, X1) & (X1 != X2)))).

#inf is the minimum general term, numerals are less than symbols, and #sup is the maximum general term:

    tff(axiom, axiom, ![N: $int]: p__less__(c__infimum__, f__integer__(N))).
    tff(axiom, axiom, ![N: $int, S: symbol]: p__less__(f__integer__(N), f__symbolic__(S))).
    tff(axiom, axiom, ![S: symbol]: p__less__(f__symbolic__(S), c__supremum__)).

Axioms Supporting External Equivalence

The standard preamble is part of every verification task. Additional axioms are added to this partial axiomatization based on the problem at hand.

Let P denote the set of problem types consisting of function constants for each placeholder in the user guide. Let F denote the set of symbolic constants (excluding placeholders) occurring anywhere in the problem. To ensure that each f in F satisfies the unique name assumption of Herbrand interpretations, we need a set of axioms O defining a total order on F. For instance, if F is {a, b, c}, then O is {a < b, b < c}. Note that a < c is a consequence of the transitivity axiom of the preamble. Additionally, we need a type declaration for every predicate in the problem (denote this set of declarations as R). We extend the standard preamble with $P \cup F \cup O \cup R$. For example, for a problem containing an integer placeholder k$, symbolic constants a and c, and predicates p/2 and q/1, we add the axioms

    tff(type, type, k$i: $int).
    tff(type, type, a: symbol).
    tff(type, type, c: symbol).
    tff(symbolic_constant_order, axiom, p__less__(f__symbolic__(a), f__symbolic__(c))).
    tff(predicate_0, type, p: (general * general) > $o).
    tff(predicate_1, type, q: (general) > $o).

Axioms Supporting Strong Equivalence

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 \[\widetilde{\forall} (hp \rightarrow tp) \]

Additional Help

Using Anthem effectively can sometimes require sophisticated proof outlines. This section has a couple of example lemmas that may help.

Absolute Lemmas

The following formulas have been established as consequences of the standard preamble. They are called “absolute lemmas” due to their origin as helpful lemmas that can apply to any problem. For difficult problems, it may help to add them as universal axioms instead of lemmas or inductive lemmas. Some must be used jointly with definitions (e.g. sqrt/1).

    axiom: I$ >= 0 -> (I$+2)*(I$+2) > (I$+1)*(I$+1) + 1.

    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: forall X, I$, J$ ( (I$ > 1 and J$ > 1 and X = I$ * J$) -> (I$ <= X and J$ <= X) ).

Reporting Bugs

To report bugs or unexpected behavior in Anthem, please email either

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
Nathan Temple

The Anthem Manual