#acl DltGroup:read,write,revert,admin GisellaBennardo:read,write All:read

-----
= DLT USER MANUAL =
----
[[TableOfContents]]

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

We can invoke the DLT system directly from the command-line, after the prompt of the system, as well the DLV system. Note that DLT relies on an external solver ES, which takes
an input generated by DLT. Models generated by ES are then parsed back to the DLT syntax. ES can be chosen from a variety of solvers (see the Compatibility Table below)


If you do not specify any options or files, DLT will just print some informational output:

{{{ > }}}'''{{{./dlt }}}'''
[[BR]]
{{{ 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] [-filter=<predicate>] [-pfilter=<predicate>] [-silent] [-solverparams={options_solver}] [filename [filename [...]]]

Specify -help for more detailed usage information.
 }}}
[[BR]]
The first line shows, first of all, the name of the executable program (DLW), 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 last three lines give a brief explanation on how to use dlt, the last line informing the user of the ''-help'' option for futher instructions.[[BR]]
[[Anchor(HELP)]]The ''-help'' or ''-h'' option[[BR]][[BR]]

{{{ > }}}'''{{{./dlt -help}}}'''  {{{   }}} or {{{  }}}  {{{ > }}}'''{{{./dlt -h}}}'''
[[BR]][[BR]]
gives the following output:
[[BR]]
{{{ DLW. Disjunctive Logic Framework for the Web
[Build DEV/May  5 2006   gcc 3.3.5 (Debian 1:3.3.5-13)]


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

DLW Specific options:

-higherorder               Enables higher order predicate names
-solver=[path_name]        The path of the solver executable file
                           For example: -solver=/dlv/dl
-preparsing                Print out re-written code and exit
-postparsing               Maps higher-order atoms into first-order atom
-filter=name1,..,nameN     Output only instances of the specified predicates
-pfilter=name1,..,nameN    Output only positive of the  instances
                           specified predicates
-solverparams={options}    The specific solver options
                           For example: -solverparams={-v -nofacts}

}}}

[[Anchor(SIL)]]
If you do not want to see this status line, use the ''-silent'' option, which suppresses various informational output and blank lines.

 {{{ > }}}'''{{{./dlt -silent}}}'''

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

Specify -help for more detailed usage information.


}}}

==== Section 1.1. DLW Specific options ====

The following table shows the specific options of DLW.[[BR]][[BR]]
'''note:''' The ''–filter'' e ''–pfilter'' options  are inherited by DLV, but they must to be considered as specific options of DLT. Indeed, DLT can change the predicate names  before passing them  to DLV ( DLT  set them up again it in the post-parsing phase ). Thus, it’s necessary that DLT performs filtering operations  directly, before printing the results. 

||< : 15% #99CCCC>  '''OPTION''' ||< : 35% #99CCCC>  '''EXPLANATION''' ||
||<: #ADD8E6> ''[#HIGH -higherorder]'' ||< #ADD8E6>Considers the names of the predicates as variables||
||<: #ADD8E6> ''-solver=[path_name]'' ||< #ADD8E6> Allows to specify the path of the solver ||
||<: #ADD8E6> ''[#PREP -preparsing]'' ||< #ADD8E6> Prints the program rewritten by DLT before sending it to solver ||
||<:  #ADD8E6> ''[#POST -postparsing]'' ||< #ADD8E6>Receives the output of the solver and maps data to the original format (before rewriting) ||
||<: #ADD8E6> ''-filter=pred''||< #ADD8E6>Turns on filtering. Predicates  pred  (or  true negated -pred ) will be included in the output. This option may be used multiple times, and pred may also be a comma-separated list of predicate names.||
||<: #ADD8E6> ''-pfilter=pred''||< #ADD8E6>Turns on filtering. Predicates named pred will be included in the output. This option may be used multiple times, and pred may also be a comma-separated list of predicate names.||
||<: #ADD8E6> ''[#SOLV -solverparams={options}]''||< #ADD8E6> In the curly brackets the user may pass the list of options for the solver separated by a space.||
||<: #ADD8E6> ''[#SIL -silent]''||< #ADD8E6>Omits the informations about the version of the executable program and the compiler ||
||<: #ADD8E6> ''[#HELP -help]'' or ''[#HELP -h]'' ||< #ADD8E6>Gives a detailed explanation on how to use DLT||

----

== Chapter 2. DLP^T Language ==

DLT's native language is [http://www.dbai.tuwien.ac.at/proj/dlv/ DLV] extended with Template predicates and other constructs. We remember that DLV's native language is ''Disjunctive Datalog'' extended with constraints, true negation, aggregates and queries.

'''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 2.1. Writing Template Definition ====

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

||< #FFFF99> '''{{{#template}}}''' ''{{{template_name}}}''{{{{}}}p,,1,,{{{(}}}a,,1,,{{{) }}}p,,n,,{{{(}}}a,,n,,{{{)}(arity)}}}[[BR]]'''{{{ { }}}'''[[BR]][[BR]] {{{       < Body of Template >      }}}[[BR]][[BR]]'''{{{ } }}}''' ||

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,,1,,(a,,1,,),..., 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 2-1. Correct Template Definitions'''

 
||< #FFFF99>'''c,,1,,''': '''{{{ #template}}}'''{{{ max{p(1)}(1)}}}[[BR]]'''{{{   { }}}'''[[BR]][[BR]]{{{   max(X) :- p(X), }}}'''{{{not}}}'''{{{ exceeded(X). }}}[[BR]][[BR]]{{{   exceeded(X) :- p(X), p(Y), Y > X. }}}[[BR]][[BR]]'''{{{   } }}}'''||


||< #FFFF99>'''c,,2,,''': '''{{{ #template}}}'''{{{ max{p(1)}(1) }}}'''{{{GLOBAL}}}'''{{{ node}}}[[BR]]'''{{{   { }}}'''[[BR]][[BR]] {{{   max(X) :- p(X), }}}'''{{{not}}}'''{{{ exceeded(X).}}}[[BR]]{{{   exceeded(X) :- p(X), p(Y), Y > X.}}}[[BR]][[BR]]'''{{{   } }}}'''||

'''Example 2-2  Wrong Template Definitions'''

||< #FFFF99>'''t,,1,,''': '''{{{ #template}}}'''{{{ wrong_definition1{p(1)}(1)}}}[[BR]]'''{{{   { }}}'''[[BR]][[BR]]{{{   exceeded(X) :- p(X), p(Y), Y > X.}}}[[BR]] {{{   p(a).}}}[[BR]][[BR]]'''{{{   } }}}'''||


||< #FFFF99>'''t,,2,,''': '''{{{ #template}}}'''{{{ wrong_definition2{-p(1), not c(1)}(1)}}}[[BR]]'''{{{   { }}}'''[[BR]][[BR]]  {{{   < Body of Template Definition > }}}[[BR]][[BR]]'''{{{   } }}}'''||

 
'''t,,1,,''' is a wrong template definition because the formal parameter ''p''cannot appear in the head of a rule.

'''t,,2,,''' 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.
 
[[Anchor(ES23)]] 
'''Example 2-3.''' The following is a template definition:
 
||< #FFFF99> #template max{p(1)}(1)[[BR]]'''{{{ { }}}'''[[BR]][[BR]]max(X) :- p(X), not exceeded(X).[[BR]]exceeded(X) :- p(X), p(Y), Y > X.[[BR]][[BR]]'''{{{ { }}}'''||


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

||< #FFFF99>'''{{{ #template }}}'''{{{max{p(1)}(1) }}}||

is the template header, and

||< #FFFF99>'''{{{ { }}}'''[[BR]][[BR]]{{{ max(X) :- p(X), not exceeded(X).}}}[[BR]]{{{ exceeded(X) :- p(X), p(Y), Y > X.}}}[[BR]][[BR]]'''{{{ } }}}'''||

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.


==== Section 2.2. Writing Template Atoms ====

We consider a generic definition of template:

||< #FFFF99>''{{{template_name}}}''{{{{}}}p,,1,,{{{(}}}X,,1,,{{{),..., }}}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,,1,,(X,,1,,),..., 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 2-4 Correct Template Atoms'''

 c,,1,,: 
||< #FFFF99>{{{ template_name{-person($,*,*)}(X).}}}||
 c,,2,,:
||< #FFFF99> {{{ template_name{person($,*,*)}(X).}}}||
 c,,3,,: 
||< #FFFF99>{{{ template_name{person(Name,*,*)}(X).}}}||
 c,,4,,:
||< #FFFF99>{{{ template_name{-person(Name,*,*)}(X).}}}||

 
'''Example 2-5  Wrong Template Atoms'''

We consider the template definition of the Example 2-3(definition of template ''max''). The following are wrong  template atoms:

 '''a,,1,,''':
||< #FFFF99>''{{{ max}}}''{{{{person(Name,*,*)}(X,Y,Z).}}}||
 '''a,,2,,''':
||< #FFFF99> ''{{{ max}}}''{{{{not person(Name,*,*)}(X).}}}||
 '''a,,3,,''':
||< #FFFF99>''{{{ max}}}''{{{{person(Name,}}}'''*''','''*'''{{{), person(}}}'''*''','''*'''{{{,$)}(X).}}}||

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

'''a,,2,,''' is a wrong template atom because the actual parameter ''person'' is preceded by negation as failure.

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


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


==== 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-6.''' The following is an example of negated and negative template atom, respectively.

||< #FFFF99> '''{{{ 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:

||< #FFFF99>'''#template'''ready_to_fire_conditions{propulsor_type(2)}(2)[[BR]]'''{{{ GLOBAL }}}'''{{{time_slot, tank, is_pressurized_by, is_damaged }}}[[BR]]{{{    { }}}[[BR]][[BR]]ready_to_fire_conditions(J,T) :- propulsor_type(J,R),[[BR]]{{{                            }}}time_slot(T),tank(TK1,R),[[BR]]{{{                            }}}tank(TK2,R), TK1 != TK2,[[BR]]{{{                            }}}is_pressurized_by(J,TK1,T),[[BR]]{{{                            }}}is_pressurized_by(J,TK2,T),[[BR]]{{{                            }}}not is_damaged(J).[[BR]][[BR]]{{{    } }}}|| 

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

||< #FFFF99> {{{ fire_jet(J,T) :- ready_to_fire_conditions{jet(*,*)}(J,T). }}}||

||< #FFFF99> {{{ fire_vernier(J,T) :- ready_to_fire_conditions{vernier(*,*)}(J,T). }}}||


==== Section 2.5. Group-by ====

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-7.''' 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-8.''' 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 [#ES23 Example 2-3]. 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 -solverparams={-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.

'''Example 2-9.''' We consider another example and the following template:

#template sum{emp(2)}(1)
{
        precedes(X,Y) :- emp(X,_), emp(Y,_), X<Y.[[BR]]
        succ(X,Y) :- precedes(X,Y), not elementInMiddle(X,Y).[[BR]]
        elementInMiddle(X,Y) :- precedes(X,Z), precedes(Z,Y).[[BR]]
        first(X) :- emp(X,_), not hasPredecessor(X).[[BR]]
        last(X) :- emp(X,_), not hasSuccessor(X).[[BR]]
        hasPredecessor(X) :- succ(Y,X).[[BR]]
        hasSuccessor(Y) :- succ(Y,X).[[BR]]
        partialSum(X,Sx) :-  first(X), emp(X,Sx).[[BR]]
        partialSum(Y,S) :-  succ(X,Y), partialSum(X,PSx), emp(Y,Sy),S=PSx+Sy.[[BR]]
        sum(S) :- last(L), partialSum(L,S).[[BR]]
}

It allows to sum all the values of the second attribute of the argument ''emp'' in an iterative manner.
The first attribute must be an ID which identifies unambiguously the instance. The template first orders the instances of ''emp'' by their ID (first rule), then using the next rules it defines the successor of each instance. It introduces a new atom, ''succ(I,II)'', thus finding the first and the last of the list (''first(X)'',''first(X)'').
The predicate ''partialSum'' scans the entire ordered list and addes the sum of the preceding values to the following value. The sum predicate receives the value associated with the last instance of ''emp''. This is possible due to the predicate ''last''.
 

Now we consider the following EDB:

employee(1,gisella,direction,80).[[BR]]
employee(2,carlo,production,36).[[BR]]
employee(3,giuseppe,administration,40).[[BR]]
employee(4,franco,distribution,45).[[BR]]
employee(5,carla,administration,45).[[BR]]
employee(6,lorenzo,direction,73).[[BR]]
employee(7,paola,production,46).[[BR]]
employee(8,marco,administration,40).[[BR]]
employee(9,gianni,production,32).[[BR]]
 

it represents a set of persons of which it is known ID, name and salary.
We use the template sum and we consider the following:

result(DIP,S):- sum{impiegato(*,$,DIP,*)}(S).

this is  a template atom which calculates the sum of the values of the 4th attribute of employee (salary) also taking into consideration the first (ID), ommiting the second(name) and grouping the result by the third attribute(department).

Launching dlt from command line, as it follows:

{{{>}}} '''{{{./ dlt name_file -silent -filter=result }}}'''

we obtain the model

{{{{result(direction,153), result(production,114), result(administration,125), result(distribution,45)}
}}}

The result is obtained in a simple manner. First, the template is executed as if the ''DIP'' parameter, which is later used to group the results, is only used for the selection. Therefore the instances of employee are ordered by their ID.  Then the ''DIP'' and salary of each are selected.  A table with a row for each employee and two columns, the first for departiment and the second for salary is obtained.  The table is then analysed dividing the rows in groups defined by their ''DIP'' values.  After this, the sum is separately calculated for each group.  The output (filtering only the ''result'' predicate) contains the sum of the salaries for each departiment. 

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

||<:tablewidth="100%">'''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,,1,,:'''{{{  head(Y) :- }}}'''{{{not}}}'''{{{ template_name{p(M,$,*)}(const).}}}

 {{{ }}}

 '''u,,2,,:'''{{{  :- }}}'''{{{not}}}'''{{{ template_name{p($,M,*)}(X).}}}

'''u,,1,,''' 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,,2,,'''  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,,1,,:'''{{{  head(Y) :- }}}'''{{{not}}}'''{{{ template_name{p(M,$,*)(const),}}}

 {{{               predicate(_,_,Y).}}}

 {{{ }}}

 '''s,,2,,:'''{{{  :- }}}'''{{{not}}}'''{{{ template_name{p($,M,*)}(X), predicate(_,_,X).}}}

 {{{ }}}
 
 '''s,,3,,:'''{{{  head(X) :- }}}'''{{{not}}}'''{{{ template_name{p(M,$,*)}(Y),}}}

 {{{               predicate(_,X,Y).}}}

 {{{ }}}

 '''s,,4,,:'''{{{  :- template_name{p(M,$,*)}(X).}}}

 {{{ }}}

 '''s,,5,,:'''{{{  :- }}}'''{{{not}}}'''{{{ template_name{p(M,$,*)}(const).}}}
----

== Chapter 4. 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 4.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. }}}

{{{     } }}}

----
[[Anchor(HIGH)]]
== Chapter 5. Higher order predicates ==

With the use of higher order predicates it is possibile to consider the names of the predicates as variables. The user inserts atoms as if they where of first order, but if the option ''-higherorder'' is used it is possible to execute higher order queries. Moreover they are fundamental for the [#HIG1 Frame Logic] and for the use of predicates that may appear with [#HIG2 different arities].

'''Example 5-1.''' We consider the following EDB: 

sister(gisella,maria).[[BR]]
mother(maria,giovanni).[[BR]]
husband(gino,carmela).[[BR]]
friend(gisella,rosina).[[BR]]
aunt(gisella,sara).[[BR]]
 
it represents a set of persons; the names of the predicates define the relations between the persons.  The use higher order allows the user to use the names of the predicates as though they where attributes of other predicates. The following rule simply rewrites the facts, but also allows the user to understand how to perform higher order queries.

relationship(X,R,Y):- R(X,Y).
 
Launching dlt from command line with option ''-higherorder'', as it follows:

{{{ > }}} '''{{{./dlt name_file -higherorder -solverparams={-nofact}}}}'''
 
we obtain the model
 
{{{
{relationship(gisella,sister,maria), 
relationship(gisella,friend,rosina), 
relationship(gisella,aunt,sara), 
relationship(maria,mother,giovanni), 
relationship(gino,husband,carmela)}
}}}

Please note that now the predicate names appear also as attributes of the relations (see for instance ''
relationship(gisella,sister,maria)'').

----

== Chapter 6. Frame Logic ==

F -logic is really useful,  since it  allows to  model reality  in a very simple way. Furthermore,  with frames   the code is  compact and the  meaning  of the program is more clear than a great  set of isolated rules. Indeed,  everything that  can be expressed  with the frames  can be without  them , but  they make the  programs more simple and intuitive. Frame Logic uses frames to represent objects. In general a frame is an object which has a name (subject) and a list of attributes, which may be empty:
 
        nomeframe[nomeattributo->valoreattributo].

'''Example 6-1.''' 
 
        mary[ spouse->john ].

The attributes may have 1 value, as in the previous example, multiple values, or they may be boolean.

'''Example 6-2.''' 

        mary[ children->>{ alice,nancy } ].
        mary[ children->>jack ].
        mary[ married ].
 
''children'' is a multivalued attribute. Its value for ''mary'' is a list including the objects ''alice'' and ''nancy''.  The second fact informs that ''mary'' has an additional child, ''jack''. It is worth noting that for multivalued attributes the notation:

        attribute->>{ value1,value2 } 

is used. This notation is also used for additional attributes.  While single variable attributes use the:

        attribute -> value

notation. Please note that in general curly brackets are not used when only one element is specified. The last clause is a boolean attribute which indicates that ''married'' is true for the object ''mary''.
 
While some attributes may be described as facts, other may be defined using inference rules.  In the previous example ''john'' is married to ''mary'' and ''mary'' has three children.  It can be assumed that ''john'' is the father of ''alice'', ''nancy'', and ''jack''. Therefore the following fact:

        john[ children->>{ alice,nancy,jack } ].
 
may be automatically derived if we add the following rule:
 
        X[ children -> C ] :- Y[ spouce->X,children->C ].
       
In addition it is possible to specify the class an object belongs to using the following rules:

        john: man.
        mary: woman.
       
Once the class of the object is identified, a specific list of attributes can be assigned at the same time:
 
        mary: woman[ children->>{ alice,nancy,jack } ].


[[Anchor(ES63)]]
'''Example 6-3.''' We consider an other definition frame: 

carlo:man[ married->camilla: woman[ children->>{ tom: man[ engaged->sara ],[[BR]]
{{{                                           }}}laura: woman[ engaged->harryT ] },[[BR]]
{{{                                }}}father->bruce ],[[BR]]
{{{         }}}children->>{ william: man[ mother->diana ],harry: man[ mother->diana ] },[[BR]]
{{{         }}}mother->elisabeth: woman,[[BR]]
{{{         }}}father->philip: man ].[[BR]]
 
The frame describes the relationships  existing between some member of  the Britannic royal family. ''carlo'' is  a ''man'' and he’s married with ''camilla''. He has two ''children'': ''william'' and ''harry'',  and their ''mother'' was ''diana''. ''carlo'' ‘s mother is ''elisabeth'' and his father is ''philip''. ''camilla'' is  a ''woman'' and she has a daughter, ''laura'', and a son, ''tom''.
''laura'' is betroth with ''harryT'' ,  and ''tom'' ’s girlfriend is ''sara''.

Launching dlt from command line:
 
{{{ > }}} '''{{{./dlt name_file}}}'''

we obtain the model

{{{
{married(carlo,camilla), children(carlo,harry), children(carlo,william), children(camilla,tom), children(camilla,laura), engaged(tom,sara), engaged(laura,harryT), man(carlo), man(tom), man(harry), man(william), woman(camilla), woman(laura), woman(elisabeth), father(carlo,philip), father(camilla,bruce), mother(carlo,elisabeth), mother(harry,diana), mother(william,diana)}
}}} 

The higher order atoms are fundamental for the frames. Indeed, the output consists of predicates whose names were attributes in the frames. For example look at the first part of the definition of the frame:

         carlo: man[ married->camilla ]

''carlo'' is a man, and he is married to ''camilla''; 'married' is an attribute of the object ''carlo'',  but in the output it's presented as the name of a predicate:

         married(carlo, camilla). 
[[Anchor(PREP)]]
Obviously, beside those defined by facts, it's possible to establish other logical relations exploiting inference rules. In this case, though, it is necessary to know how the frames were written, since the user must write the rules using the atoms in the same format.
It is possible to know how a frame is rewritten, using the option ''-preparsing''. Executing the  previous example using ''-preparsing'' the program is rewritten and returned in output. The inference rules must be written based on the atoms given in output.

Launching a program with ''-preparsing'' option:

{{{ > }}} '''{{{./dlt nome_file -preparsing}}}'''

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

% LEGENDA OF TEMPLATE INVOCATIONS
% END OF LEGENDA
married(carlo,camilla).
children(camilla,tom).
fidanz(tom,sara).
man(tom).
children(camilla,laura).
fidanz(laura,harry).
woman(laura).
father(camilla,bruce).
woman(camilla).
children(carlo,william).
mother(william,diana).
man(william).
children(carlo,harry).
mother(harry,diana).
man(harry).
mother(carlo,elisabetta).
woman(elisabetta).
father(carlo,philip).
man(carlo).
}}}

At this point it's simple to determine which atoms must be used for the query. If we wish to know the grandchildren of the Queen Elisabeth, the following rule would suffices:

        grandmother(X,Y):-mother(Z,X),children(Z,Y).

X (elisabetta, in this case) is the grandmother of Y(william and harry, in this case) if there exists a Z(carlo, in this case) which is the child of  X and the father of Y.

With the addition of this rule we obtain:

{{{ > }}} '''{{{./dlt  nome_file -solverparams={-filter=grandmother}}}}'''

{{{{grandmother(elisabetta,harry), grandmother(elisabetta,william)}
}}}
 
As expected Elisabeth is the grandmother of harry and william, the children of carl.
 

'''Example 6-4.''' Let's show another example:

gianni:studente[
                pc->mistero:notebook[
                                     os->debian:os[
                                                   kind->gnu,
                                                   kernel->linux]]].
 [[Anchor(HIG2)]] 
The frame says that Gianni is a student and has a pc named mistery.  The pc is a notebook which uses debian as operating system.  In addition information on the OS is given: kind and kernel. Launching this program without the option higherorder results with an error:
 
{{{ > }}} '''{{{./dlt nome_file}}}'''

{{{       
os, first used with arity 2, now seen with arity 1.
 }}}

The cause of the error is clear once we look at the opuput with the option -higherorder

{{{ > }}} '''{{{./dlt -higherorder nome_file}}}'''
{{{
{pc(gianni,mistero), os(mistero,debian), kind(debian,gnu), kernel(debian,linux), os(debian), notebook(mistero), studente(gianni)}
}}}

The atoms os(mistero,debian) e os(debian) appears in the output. The same predicate is present with different arity. In the case of first order atoms this is not permitted.  It is only possible using higher order atoms.
 
==== Section 6.1. Frame Space directive ====

The Frame Space is a new directive introduced in DLT:

''@name.''
      From the point after the directive each frame is interpreted as 
      belonging to the frame space 'name'. A frame
      X[f->Y] is rewritten as f(X,Y,name).
''@.''
      Cancels out the default Frame Space. Goes back to the normal 
      rewriting X[f->Y] = f(X,Y).
----

== Chapter 7. System Architecture ==

A DLP^T^ program P, 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 SOLVER program P'; P' is piped towards the SOLVER system. The models M(P') of P', computed by SOLVER, 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.

'''Figure 1.'''

attachment:flow.gif 
  
==== Section 7.1 DLT Work-Flow ====

We show here the work-flow of DLT, exploiting [#ES63 example 6-3]. We launch the program with ''-preparsing'' option and divert the output in the file (''tmp''):[[BR]]
[[Anchor(HIG1)]] 
{{{ > }}} '''{{{./dlt -silent -higherorder -preparser nome_file >tmp}}}'''

The file ''tmp'' will appear as following:  

{{{
% LEGENDA OF TEMPLATE INVOCATIONS
% END OF LEGENDA
a_2(married,carlo,camilla).
a_2(children,camilla,tom).
a_2(engaged,tom,sara).
a_1(man,tom).
a_2(children,camilla,laura).
a_2(engaged,laura,harryT).
a_1(woman,laura).
a_2(father,camilla,bruce).
a_1(woman,camilla).
a_2(children,carlo,william).
a_2(mother,william,diana).
a_1(man,william).
a_2(children,carlo,harry).
a_2(mother,harry,diana).
a_1(man,harry).
a_2(mother,carlo,elisabeth).
a_1(woman,elisabeth).
a_2(father,carlo,philip).
a_1(man,philip).
a_1(man,carlo).
}}}

Passing the content of ''tmp'' to the solver (i.e., DLV in this case) and diverting the output in another file (''tmp2''):

{{{ > }}} '''{{{./dl -silent tmp > tmp2}}}'''

the file ''tmp2'' will look as following: 

{{{
{a_2(married,carlo,camilla), a_2(children,carlo,william), a_2(children,carlo,harry), a_2(children,camilla,tom), a_2(children,camilla,laura), a_2(engaged,tom,sara), a_2(engaged,laura,harryT), a_2(father,carlo,philip), a_2(father,camilla,bruce), a_2(mother,carlo,elisabeth), a_2(mother,william,diana), a_2(mother,harry,diana), a_1(man,carlo), a_1(man,tom), a_1(man,william), a_1(man,harry), a_1(man,philip), a_1(woman,camilla), a_1(woman,laura), a_1(woman,elisabeth)}
}}}
[[Anchor(POST)]]
Finally, we send the content of ''tmp2'' to DLT postparser module as following: 

{{{ > }}} '''{{{./dlt -postparsing <tmp2 }}}'''

and we obtain the following:

{{{
{married(carlo,camilla), children(carlo,william), children(carlo,harry), children(camilla,tom), children(camilla,laura), engaged(tom,sara), engaged(laura,harryT), father(carlo,philip), father(camilla,bruce), mother(carlo,elisabeth), mother(william,diana), mother(harry,diana), man(carlo), man(tom), man(william), man(harry), man(philip), woman(camilla), woman(laura), woman(elisabeth)}
}}}

the same output that we would have obtained launching the command:

{{{ > }}} '''{{{./dlt family}}}'''

Indeed, performing the whole process launching directly DLT as above, the only model is:

{{{
{married(carlo,camilla), children(carlo,william), children(carlo,harry), children(camilla,tom), children(camilla,laura), engaged(tom,sara), engaged(laura,harryT), man(carlo), man(tom), man(william), man(harry), man(philip), woman(camilla),woman(laura), woman(elisabeth), father(carlo,philip), father(camilla,bruce), mother(carlo,elisabeth), mother(william,diana), mother(harry,diana)}
}}}
   
exactly the same of what obtained performing explicitly all the operations constituting the flow.
                                 
==== Section 7.2. Compatibility with other solvers ====
[[Anchor(SOLV)]]
DLT can virtually support any solver. At the moment, we can state the compatibility with the syntax of some of them. The following table shows the instructions of the solvers which dlt natively recognizes.

||< : 15% #99CCCC>  '''SOLVER''' ||< : 15% #99CCCC>  '''WHAT'S SUPPORTED''' ||< : 15% #99CCCC> '''SYNTAX'''||
||< : #ADD8E6> ''any solver'' ||<: #ADD8E6> ASITIS ||<: #ADD8E6> ASITIS%* Body *% [[BR]] ''ASITIS's Body is sent verbatim to solver''||
||< : #ADD8E6> ''dlv'' ||<: #ADD8E6> Aggregates and weak constraints  ||<: #ADD8E6> see   [http://www.dbai.tuwien.ac.at/proj/dlv/man/ DLV - User Manual ]||
||< : #ADD8E6> ''dlv+odbc'' ||<: #ADD8E6> Not tested yet  ||<: #ADD8E6> see   [http://www.dbai.tuwien.ac.at/proj/dlv/man/ DLV - User Manual ]||
||< : #ADD8E6> ''dlvex'' ||<: #ADD8E6>external built-ins  ||<: #ADD8E6> see   [http://www.mat.unical.it/ianni/wiki/dlvex?action=AttachFile&do=get&target=usermanual.html dlvex - User Manual ] ||
||< : #ADD8E6> ''dlvhex'' ||<: #ADD8E6>external atoms, namespace directive||<: #ADD8E6> see   [http://con.fusion.at/dlvhex/ dlvhex - User Manual ] ||
||< : #ADD8E6> ''smodels'' ||<: #ADD8E6> Supports normal programs with function symbols ||<: #ADD8E6> see   [http://www.tcs.hut.fi/Software/smodels/ smodels - User Manual ] ||

'''Note:'''  All the SOLVER options must be passed using the option ''-solverparams={}''. 
==== Section 7.3. Notes on using DLV-HEX with DLT ====
DLV-HEX has higher order reasoning built-in, so it is not necessary to invoke DLT with the option {{{-higherorder}}} switched on. Also, DLV-HEX supports natively DLT. DLT can be
used with DLV-HEX with different command line combinations such as

{{{
   dlt -silent -preparsing program.dlt | dlvhex -- | dlt -postparsing
}}}

or

{{{
   dlvhex -dlt program.dlt
}}}

makes dlvhex to invoke dlt as a preparser