DLT USER MANUAL

Overview

DLT is a front-end for disjunctive datalog, extending the DLV system with Template predicates, Frame Logic and higher order predicate names. Template predicates can be seen as a way to define intensional predicates by means of a subprogram, where the subprogram is generic and reusable as many times is necessary. Frame Logic extends classical logic and it gives consent for frame-based or object–oriented syntax. Higher order predicates allow to treat predicate names as variables (although this semantics has quite nothing to deal with second order logics). The language implemented by the DLT system is named DLP^T.BR

More information (including an online version of this manual and an online tutorial) and the executable program for Linux platform are available at the DLT homepage (http://dlt.gibbi.com).[[BR]]

Chapter 1. Getting Started

You can invoke the DLT system directly from the command-line, after the prompt of the system, as well the DLV system.

Note: All the DLV options must be passed using the option -solverparams={}. In the curly brackets the user may pass the list of options for the solver separated by a space.

If you do not specify any options or files, DLT will just print some informational output and an empty model ({ }):

>'''{{{./dlt

DLW. Disjunctive Logic Framework for the Web [Build DEV/May 3 2006 gcc 3.3.5 (Debian 1:3.3.5-13)]

usage: ./dlt {FRONTEND} {OPTIONS} [-higherorder] [-solver=<path>] [-preparsing] [-postparsing] [-solverparams={options_solver}] [filename [filename [...]]]

Specify -help for more detailed usage information.

}}}

The first line shows, first of all, the name of the executable program (DLT), then it gives information about the version of the executable program, the date when the binary was built and the identifier of the compiler. The identifier BEN, which stands for "benchmark version".

Note: Versions other than BEN should only be used for development purposes!

Usually, you will not have to bother with these gory details, but please include this information when you are reporting a bug or asking for support.

If you do not want to see this status line, use the -silent option, which suppresses various informational output and blank lines.

$ dlt -silent
{}

From now on, all examples will include the -silent option.

Chapter 2. DLP^T Language

DLT’s native language is DLV extended with Template predicates. We remember that DLV’s native language is Disjunctive Datalog extended with constraints, true negation, aggregates and queries.

Section 2.1. Template Definition

A template definition D consists of a template header and an associated DLP^T subprogram closed into parenthesis curly braces.

Example 2-1. The following is a template definition:

 #template max[p(1)](1)
 {
    max(X) :- p(X), not exceeded(X). 
    exceeded(X) :- p(X), p(Y), Y > X. 
 }

This template introduces a generic template program, defining the predicate max, intended to compute the maximum value over the domain of a generic unary predicate p. In this example we have that

#template max[p(1)](1)

is the template header, and

{
max(X) :- p(X), not exceeded(X).
exceeded(X) :- p(X), p(Y), Y > X.
}

is a DLP^T subprogram. max is the template name; p is a predicate name, called formal predicate. The arity of formal predicate p is 1 and the output arity of template definition is 1.

Note: The DLP^T subprogram may contain disjunctive rules, constraints, weak constraints, aggregates, built-in predicates, negative literals, true negation, template atoms (or invocations), and it do not contains template definitions.

Example 2-2. Wrong Template Definition

The following is not a valid template definition:

#template wrong_definition[p(1)](1)
{
template max[h(1)](1)
< other rules >
}

Section 2.2. Template Atom

A template definition may be instantiated as many times as necessary, trough template atoms. The template atom or invocation consists of a template name, a list of atom and a list of variables and/or constants (literal constants and numerical constants).

Example 2-3. The followings are template atoms:

max[weight(*)](M)
max[student($,Sex,*)](Age)

max is the template name; weight and student are predicate names, called actual predicates; variables and constants are called standard terms (Sex is a standard term); the dollar ‘$’ symbol is called projection term and the symbol ‘*’ is called parameter term. M and Age are a list of usual terms (i.e. either variables or constants), and are called output lists.

We note that the template definitions may be unified with a template atom in many ways. The above example contains a plain invocation (max[weight(*)](M)), and a compound invocation (max[ student($,Sex,*) ](Age)). Intuitively, projection terms (‘$’ symbols) are intended in order to indicate attributes of an actual predicate which have to be ignored. A standard term (a constant or a variable) within an actual atom indicates a ‘group-by’ attribute, whereas parameter terms (‘*’ symbols) indicate attributes to be considered as parameter.

For example, the template atom max[student($,Sex,*)](Age) allows to employ the definition of the template predicate max on a ternary predicate student, discarding the first attribute of student, and grouping by values of the second attribute. The intuitive meaning of this invocation is to define a predicate computing the student with maximum value of the ‘Age’ attribute (the third attribute of the student predicate), grouped by the ‘Sex’ attribute (the second one), ignoring the first attribute. The computed values of Age are returned through the output list.

Example 2-4. We consider the following EDB:

person(riccy,f,26).
person(kali,f,26).
person(peppe,m,26).
person(gibbi,m,29).
person(paddy,f,27).

it represents a set of persons of which it is known name, sex and age. We consider the template definition of max given in Example 2-1. The following:

older_sex(Name,Sex,Age):- max[person($,Sex,*)](Age),
person(Name,Sex,Age).

is a template atom that compute the oldest person with grouping on the sex attribute, that is the person of age greater than female sex and that one of male sex. Launching dlt from command line, as it follows:

$ dlt -silent -nofacts programFileName

we obtain the model

{older_sex(paddy,f,27),older_sex(gibbi,m,29)}

Therefore paddy is the greatest person of female sex, while gibbi is the greateest person of male sex.

Section 2.3. Negative Rules with Template Atoms and True Negation

Template atoms can be used also as negated and negative atoms in the generic rules of the program. Then we can use a template atom after the “negation as failure” symbol (not) as it happens for the usual atoms.

Example 2-5. The following is an example of negated and negative template atom, respectively.

not max[student(Sex,$,*)](Age)

Negation for template atoms is treated as well negation for DLV atom. For more information about “negation as failure” and true negation we send back at the DLV user manual available at the DLV homepage (http://www.dbai.tuwien.ac.at/proj/dlv/).

Section 2.4. Template Definition with Global Predicates

Template programming can become a very useful feature in applications where it is necessary to compact repetitive pieces of code. We consider a planning program for the Space Shuttle Reaction Control System. Here is a sketch from the program:

#template ready_to_fire_conditions[propulsor_type(2)](2)

GLOBAL time_slot, tank, is_pressurized_by, is_damaged

{

ready_to_fire_conditions(J,T) :- propulsor_type(J,R), }

time_slot(T),tank(TK1,R),

tank(TK2,R), TK1 != TK2,

is_pressurized_by(J,TK1,T),

is_pressurized_by(J,TK2,T),

not is_damaged(J).

}

the above template is employed to remove a set of repeated rules, which are changed this way

fire_jet(J,T) :- ready_to_fire_conditions[jet(*,*)](J,T).

fire_vernier(J,T) :- ready_to_fire_conditions[vernier(*,*)](J,T).

Chapter 3. Safety

Safety of variables in template atom follows the usual criterion. We suppose to have in the body of a generic rule a negated invocation; then must be valid the following condition must be valid:

Safety for the Negated Template Atom

Each variable occurring in the output list of the given invocation also occurs in at least one non-comparative positive literal in the body of the same rule (resp. the same constraint).

Example 3-1. Unsafe Rules and Constraints

u₁: head(Y) :- not template_name[p(M,$,*)](const).

u₂: :- not template_name[p($,M,*)](X).

u₁ is unsafe because the variable ‘Y’ that appear in the head of the rule does not appear in at least a positive atom of the body of the same rule.

u₂ is unsafe because the variable ‘X’ in the output list of the given invocation does not appear in at least a positive atom of the body of the same rule.

Example 3-2. Safe Rules and Constraints

s₁:  head(Y) :- not template_name[p(M,$,*)](const),
               predicate(_,_,Y).

s₂:  :- not template_name[p($,M,*)](X), predicate(_,_,X).
s₃:  head(X) :- not template_name[p(M,$,*)](Y),
               predicate(_,X,Y).

s₄:  :- template_name[p(M,$,*)](X).

s₅:  :- not template_name[p(M,$,*)](const).

Chapter 4. Using DLP^T Language

How to write a DLP^T program?

For a correct writing and usage of the DLP^T language here are a few general conditions that must be satisfied.

Section 4.1. Writing Template Definition

We consider a generic definition of template:

#template template_name[p₁(a₁),..., p_n(a_n)](arity)
    {
    < Body of Template >
    }

All the following conditions must be respected:

In the body of a template definition at least a rule must have an atom in its head with the same name of the template in which it is defined;
The formal parameters (p₁(a₁),..., p_n(a_n)) cannot appear in a head;
All the formal parameters should appear in some rules;
In the program cannot exist two or more template definitions having the same name;
The formal parameters cannot be preceded from the true negation symbol and the negation as failure simbol in the template header in which they are uses;
The global predicates defined using the GLOBAL directive cannot appear in the head of a rule defined in the body of the template;
Definitions of template cannot appear in the body of a template;

Example 4.1. Wrong Template Definitions

t₁: #template wrong_definition1[p(1)](1)
-    {
     exceeded(X) :- p(X), p(Y), Y > X.
     p(a).
     }
t₂: #template wrong_definition2[-p(1), not c(1)](1)
-    {
     < Body of Template Definition >
     }

t₁ is a wrong template definition because the formal parameter ‘p’ cannot appear in the head of a rule.

t₂ is a wrong template definition because the formal parameter ‘p’ is preceded from the true negation symbol, while the formal parameter ‘c’ is preceded from the negation as failure symbol.

Example 4.2 Correct Template Definitions

c₁: #template max[p(1)](1)
-    {
     max(X) :- p(X), not exceeded(X).
     exceeded(X) :- p(X), p(Y), Y > X.
     }
c₂: #template max[p(1)](1) GLOBAL node
-    {
     max(X) :- p(X), not exceeded(X).
     exceeded(X) :- p(X), p(Y), Y > X.
     }

Section 4.2. Writing Template Atoms

We consider a generic definition of template:
template_name[p₁(X₁),..., p_n(X_n)](Args)
All the following conditions must be respected:
For every template atom, defined in some rule of the general program, there must exist a definition having the same name of template_name;
The number of actual predicates (p₁(X₁),..., p_n(X_n)) must be equal to the number of formal predicates of the correspondent definition;
The arity of the output terms must be equal to the output arity of the correspondent definition;
The number of asterisks of every actual parameter must be equal to the arity of the correspondent formal parameter;
The actual parameters cannot appear negated in the atom template that uses them(note that true negation is allowed instead).

Example 4.3 Wrong Template Atoms

We consider the template definition of the Example 2-1(definition of template ‘max’). The following are wrong template atoms:

a₁: max[person(Name,*,*)](X,Y,Z).

a₂: max[not person(Name,*,*)](X).

a₃: max[person(Name,*,*), person(*,*,$)](X).

a₁ is a wrong template atom because the arity of the output terms is not equal to the output arity of the correspondent definition.

a₂ is a wrong template atom because the actual parameter ‘person’ is preceded by negation as failure.

a₃ is a wrong template atom because the number of actual predicates is not equal to the number of formal predicates of the correspondent definition.

Example 4.4 Correct Template Atoms

c₁: template_name[-person($,*,*)](X).

c₂: template_name[person($,*,*)](X).

c₃: template_name[person(Name,*,*)](X).

c₄: template_name[-person(Name,*,*)](X).

Chapter 5. System Architecture

The DLP^T language has been implemented on top of the DLV system. The overall architecture of the system is shown in Figure 1. A DLP^T program is sent to a DLP^T pre-parser, which performs syntactic checks (included nonrecursivity checks), and builds an internal representation of the DLP^T program. The DLP^T Inflater produces an equivalent DLV program P’; P’ is piped towards the DLV system. The models M(P’) of P’, computed by DLV, are then converted in a readable format through the Post-parser module; the Post-parser filters out from M(P’) informations about internally generated predicates and rules.

Chapter 6. Knowledge Representation by DLP^T

In this section we show by example the main advantages of template programming. Example put in evidence the easiness of providing a succinct and elegant way for quickly introducing new constructs using the DLP^T language.

Section 6.1. Aggregates

Aggregate predicates allow to represent properties over sets of elements: the next example shows how to fast prototype aggregate semantics without taking into account of the efficiency of a built-in implementation.Here we take advantage of the template predicate max, defined in Example 2.1. The next template predicate defines a general program to count distinct values of a predicate p, given an order relation succ defined on the domain of p.

#template count[p(1),succ(2)](1)

{

partialCount(0,0).

partialCount(I,V) :- not p(Y), I=Y+1,partialCount(Y,V).

partialCount(I,V2) :- p(Y), I=Y+1,partialCount(Y,V),

succ(V,V2).

partialCount(I,V2) :- p(Y),I=Y+1,partialCount(Y,V),

max[succ(*,$)](V2).

count(M) :- max[partialCount($,*)](M).

}

The above template definition is conceived in order to count, in a iterative-like way, values of the p predicate through the partialCount predicate. A ground atom partialCount(i,a) means that at the stage i, the constant a has been counted up. The predicate count takes the value which has been counted at the highest (i.e. the last) stage value. It is worth noting how max is employed over the binary predicate partialCount, instead of an unary one. Indeed, the ‘$’ and ‘*’ symbols are employed to project out the first argument of partialCount. The last rule is equivalent to the piece of code:

partialCount'(X) :- partialCount(_,X).

count(M) :- max[partialCount'(*)](M).

Template definitions can be employed to introduce and reuse constructs defining the most common search spaces. This improves declarativity of ASP programs to a larger extent. The next two examples show how to define a predicate subset and a predicate permutation, ranging, respectively, over subsets and permutations of the domain of a given predicate p.

#template subset[p(1)](1)

{

subset(X) v -subset(X) :- p(X).

}

#template permutation[p(1)](2).

{

permutation(X,N)v npermutation(X,N) :- p(X),#int(N), N <= N1,

count[p(*),>(*,*)](N1).

:- permutation(X,A),permutation(Z,A), Z <> X.

:- permutation(X,A),permutation(X,B), A <> B.

covered(X) :- permutation(X,A).

:- p(X), not covered(X).

}

The explanation of the subset template predicate is quite straightforward. As for the permutation definition, a ground atom permutation(x,i) tells that the element x (taken from the domain of p), is in position i within the currently guessed permutation. The rest of the template subprogram forces permutations properties to be met.

Next we show how count and subset can be exploited to succinctly encode the k-clique problem, i.e., given a graph G (represented by predicates node and edge), find if there exists a complete subgraph containing at least k nodes (we consider here the 5-clique problem):

in_clique(X) :- subset[node(*)](X).

:- count[in_clique(*),>(*,*)](K),K < 5.

:- in_clique(X),in_clique(Y), X <> Y, not edge(X,Y).

The first rule of this example guesses a clique from a subset of nodes. The first constraint forces a candidate clique to be at least of nodes, while the last forces a candidate clique to be strongly connected. The permutation template can be employed, for instance, to encode the Hamiltonian Path problem: given a graph G, find a path visiting each node of G exactly once:

path(X,N) :- permutation[node(*)](X,N).

:- path(X,M), path(Y,N), not edge(X,Y), M = N+1.

Sets: Extending Datalog with Set programming is another matter of interest for the ASP field. It is fairly quick to introduce set primitives using DLP^T; a set S is modeled through the domain of a given unary predicate s. Intuitive constructs like intersection, union, or symmetricdifference, may be modeled as follows.

#template intersection[a(1),b(1)](1).

{

intersection (X) :- a(X),b(X).

}

#template union[a(1),b(1)](1).

{

union(X) :- a(X). union(X) :- b(X).

}

#template symmetricdifference[a(1),b(1)](1)

{

symmetricdifference(X) :- union[a(*),b(*)](X),

not intersection[a(*),b(*)](X).

}

Dates: managing time and date data types is another important issue in engineering applications of DLP. The following template shows how to compare dates represented through a ternary relation day, month, year.

#template before[date1(3),date2(3)](6) }}}

{

before(D,M,Y,D1,M1,Y1) :- date1(D,M,Y),

date2(D1,M1,Y1), Y < Y1.

before(D,M,Y,D1,M1,Y1) :- date1(D,M,Y),

date2(D1,M1,Y1), Y == Y1, M < M1.

before(D,M,Y,D1,M1,Y1) :- date1(D,M,Y), date2(D,M1,Y1),

Y == Y1, M = M1, D < D1.

}