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

Natural Translation (nu)

The tau* transformation often produces complex formulas. For a broad class of mini-gringo programs called regular, an alternative translation known as nu (ν) is available via the translate command:

    anthem translate program.lp --with nu

For regular rules, the resulting formulas are much simpler while still retaining HT-equivalence to their τ* counterparts. This transformation was introduced here.

A Combined Transformation (mu)

The mu (μ) translation is obtained by applying ν to every regular rule, and tau* to the remainder. A justification for this process can be found here. It can be accessed as a translation option as follows:

    anthem translate program.lp --with mu

Since anthem refuses to compute νΠ when Π is not regular, μ is usually a better option.

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.

The Anthem Manual