Francisco Coelho / zugzwang

ASP-DLV_tutorial.html 42.1 KB
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 
<html>
<head>
<BASE HREF="http://www.dlvsystem.com/tutorial/">

<title>The DLV Tutorial</title>
</head>
<body BGCOLOR="#ffffff" LINK="#000099">
<!font face="Arial, sans-serif">


<h2>
The <b><code>DLV</code></b> Tutorial
</h2>

In this tutorial, we give an introduction to <em>Disjunctive Datalog</em>
(using some of the extensions of <b><code>DLV</code></b>).
The tutorial does not give a full description of the usage and capabilities of
<b><code>DLV</code></b>.
For a more complete account of these, see the
<a href="http://www.dlvsystem.com/"><b><code>DLV</code></b>
homepage</a> and the
<a href="http://www.dlvsystem.com/man/">
<b><code>DLV</code></b> online user manual</a>.

The examples shown in this tutorial work with every recent
<b><code>DLV</code></b> release.
Executables of the <b><code>DLV</code></b> system for various platforms
can be downloaded from the
<a href="http://www.dlvsystem.com/">
<b><code>DLV</code></b> homepage</a>.
<p>

The tutorial consists of the following sections, each of them being built
around a guiding example:

<ul>
<li> The First Example : Rules and Facts </li>
<li> The Second Example : Negation and the Complete World Assumption </li>
<li> The Family Tree Example : Predicates, Variables, and Recursion </li>
<li> <code>DLV</code> as a Deductive Database System; Comparison Operators </li>
<li>
The Railway Crossing Example : True Negation and Negation as Finite Failure
</li>
<li>
The Broken Arm Example : Disjunctive Datalog and the Stable Model Semantics
</li>
<li> Strong Constraints </li>
<li> Graph Coloring: Guess&Check Programming </li>
<li> The Fibonacci Example: Built-in Predicates and Integer Arithmetics </li>
<li> The 8-Queens Example: Guess&Check Programming with Integers </li>
<li> A simple Physics Diagnosis example </li>
<li> A different way to implement the Physics Diagnosis example </li>
<li> The Monkey&Banana Example: Planning </li>
</ul>

This page is quite long. People who are in a hurry might appreciate the
information that the tutorial is fully on this page, there will be no branches
and no links to further pages.
<p>

<b>This tutorial is written for computer-literate people with a background
different from computer science, or students new to this area.
It was originally written for physicists at CERN, and some examples are
tailored towards this community.</b>
<p>


<hr>
<h3>
Introduction
</h3>

<p>
Datalog is a <em>declarative</em> (programming) language.
This means that the programmer does not write a program that solves some
problem but instead specifies what the solution should look like, and a
Datalog inference engine (or <em>Deductive Database System</em>) tries
to find the the way to solve the problem and the solution itself.
This is done with <em>rules</em> and <em>facts</em>.
Facts are the input data, and rules can be used to derive more facts, and
hopefully, the solution of the given problem.
</p>

<p>
Disjunctive datalog is an extension of datalog in which the logical OR
expression (the disjunction)
is allowed to appear in the rules - this is not allowed in basic datalog.
</p>

<p>
<b><code>DLV</code></b> (= datalog with disjunction) is a powerful though
freely available deductive database system.
It is based on the declarative programming language <em>datalog</em>,
which is known for being a convenient tool for knowledge representation.
With its disjunctive extensions, it is well suited for all kinds of
nonmonotonic reasoning, including diagnosis and planning.
</p>

<p>
Finally, we have to mention to the more advanced reader that
<b><code>DLV</code></b> is relevant to two communities. Firstly, as mentioned,
it is a deductive database engine and can therefore be seen as a way to query
data from databases which is strictly more powerful than for example SQL
(everything that can be done with the core SQL language can also be done with
<b><code>DLV</code></b>, and more), but it is also often described as a
system for answer set programming (ASP). This is a powerful new paradigm
from the area of "Nonmonotonic Reasoning" which allows to formulate even very
complicated problems in a straightforward and highly declarative way.
One may call this paradigm even more declarative than classical logic.
Of course, every programming language to be processed by a computer has to
have both fixed syntax (i.e. a grammar that specifies what programs of this
language have to look like, and what combinations of symbols make a valid
program) and semantics (which abstractly specifies what the computer has to
do with the program by declaring how a program is to be translated into the/a
correct result). There is wide agreement (and also some excitement) that
both the syntax and semantics of the language of <b><code>DLV</code></b>
are very simple and intuitive. In fact, we do not know of any way to make
the language even simpler while preserving its characteristics.
</p>

<p>
Both the syntax and semantics of <b><code>DLV</code></b> will be described in
this tutorial.
</p>


<hr>
<h3>
The First Example : Rules and Facts
</h3>

<p>
Suppose we want to model that every time somebody tells us a joke, we laugh.
Furthermore, somebody now tells us a joke.
This could be done in the following way:

<blockquote><pre>
joke.
laugh :- joke.
</pre></blockquote>

The first line is called a fact and expresses that <code>joke</code>
is true (a simple word such as <code>joke</code> appearing in a rule or fact
which has a truth value is called a <em>proposition</em>. A more general
name - which we will use in the following - for the constituents of rules
and facts is <em>atom</em>.).
The second line is called a rule.
It is read as "if joke is true, laugh must also be true".
(The sign ":-" is meant to be an arrow to the left, the logic programming
version of the implication.)
</p>

<p>
If the author of such a program decides it appropriate, one can also interpret
some causality into a rule and read this one as "from joke follows laugh".
This is pure matter of choice of the human, and <b><code>DLV</code></b>
does not care about it.
The left side of a rule is called its <em>head</em>, while the right side is
called its <em>body</em>.
</p>

<p>
A result of a Datalog computation is called a <em>model</em>.
The meaning of this is clear: it is a consistent explanation (model)
of the world, as far as the Datalog system can derive it.
If a datalog program is inconsistent, i.e., it is contradictory, there is
simply no model (we will see examples of this later).
</p>

<p>
Of course, since in this example <code>joke</code> is certainly true (this is
given by the fact), <code>laugh</code> is also true.
<code>DLV</code> now tries to find all those models of the world that correctly
and consistently explain the observations made (= the program).

A model assigns a truth value (either <em>true</em> or <em>false</em>) to
each atom appearing in the program,
and is written as the set of atoms that are true in a certain model.
The model of the above program is <code>{joke, laugh}</code>.
When all atoms are false in a model, we talk about an empty model
(written as <code>{}</code>). Note that having an empty model is very different
from finding no model. We will see examples for this later.
</p>

<p>
Simple datalog programs like the one above always have exactly one model.
In general, though, <b><code>DLV</code></b> programs may have zero
(as mentioned) or even many models. We will see examples of such programs later.
</p>



<hr>
<h3>
The Second Example : Negation and the Complete World Assumption
</h3>

<p>
Next, suppose we are not aware of being told a joke. In this case, the
correct datalog program looks like this:

<blockquote><pre>
laugh :- joke.
</pre></blockquote>

The program itself does not express that joke is false, but the so-called
<em>Complete World Assumption (CWA)</em> does. It is one of the foundations
<code>DLV</code> bases its computations on and says that everything about which
nothing is known is assumed to be false.
Therefore, the model for this program is <code>{}</code>. (This means that
there is a model but it is empty. It is also possible that for a given
program there is no model.)
We will come back to the CWA in more detail later in the section that
discusses <code>DLV</code> as a deductive database system.
</p>

<p>
Next, we elaborate a bit on this example.
First, we want to express that to be able to understand a joke, one has to 
hear it and must not be stupid. To hear it, one must not be deaf and there
must be a joke.
Finally, to laugh about the joke, one must understand it.
Alternatively, stupid people might laugh without being told a joke.

<blockquote><pre>
joke.
hear_joke :- joke, not deaf.
understand_joke :- hear_joke, not stupid.
laugh :- understand_joke.
laugh :- stupid, not joke.
</pre></blockquote>

In two of the rules, we encounter negated atoms. These are true if the
atoms themselves are false.
We also encounter rules that contain more than one atom in the
body. In such a case, a body is true if each of the literals are true
(a literal is a possibly negated atom).
For example,

<blockquote><pre>
hear_joke :- joke, not deaf.
</pre></blockquote>

is read as
"if <code>joke</code> is true and <code>deaf</code> is false then
<code>hear_joke</code> must be true".
</p>

<p>
The model for this program is
<code>{joke, hear_joke, understand_joke, laugh}</code>.
Again, by virtue of the CWA, <code>deaf</code> and <code>stupid</code>
are assumed to be false - there are no facts making these atoms 
true and no rules which can derive their truth.
Now suppose we remove <code>joke.</code> from the program and add
<code>stupid.</code> instead. Then, the resulting model would be
<code>{stupid, laugh}</code>.
</p>

Please note the following things:
(i) Those atoms that are not listed as elements of the models above are
<em>not</em> automatically rendered false. Rather, they are unknown.
(ii) Suppose the program would look like this:

<blockquote><pre>
stupid.
laugh :- stupid, not joke.
</pre></blockquote>

The model of this program is <code>{stupid, laugh}</code>. If we now add the
fact <code>joke.</code> we get the model <code>{stupid, joke}</code>, from
which the atom <code>laugh</code> got lost. In other words, you may add
more information and lose information that could be derived before because of
that. Due to this property,
the formalism of <b><code>DLV</code></b> is called <em>nonmonotonic</em>, just
as mathematical functions which are neither monotonically increasing nor
decreasing are called nonmonotonic.

At first sight, this may look like an ugly property of this formalism, but in
fact, it allows to do many useful things.
</p>



<hr>
<h3>
The Family Tree Example : Predicates, Variables, and Recursion
</h3>

So far we have studied simple atoms as the building blocks of our rules.
In fact, atoms may be constructed to hold a number of arguments - they are
then also called <em>predicates</em>.
<p>

In the following program, we have two binary predicates, <code>parent</code>
and <code>grandparent</code>. (They are called binary because they both have
two arguments.)
<p>

We have to map some semantics to the two arguments of the predicates. Here,
the first argument is assumed to be the older person
(the parent or grandparent), while
the second argument refers to the younger person (the child or grandchild).
Certainly, we could do it the other way as well, but then we would have to
adjust all the rules that will follow.

<blockquote><pre>
parent(john, james).
parent(james, bill).
grandparent(john, bill) :- parent(john, james), parent(james, bill).
</pre></blockquote>

Of course, the model of this program is
<code>{parent(john, james), parent(james, bill), grandparent(john,bill)}</code>.

<p>
With predicates, it is allowed to use variables, which begin with an upper-case
character, differently from the constants of the previous program that begin
with a lower-case letter. The following program has the same model as the
previous example:

<blockquote><pre>
parent(john, james).
parent(james, bill).
grandparent(X, Y) :- parent(X, Z), parent(Z, Y).
</pre></blockquote>

This new grandparent rule which uses variables simply models that every
parent of a parent is a grandparent.
</p>

<p>
Note that the facts of a program are often called the
<em>Extensional Database (EDB)</em>, while the remaining rules are called
the <em>Intensional Database (IDB)</em>.
With <b><code>DLV</code></b>, the EDB can be read either from a relational
or object-oriented database, or just simply from files, where no separation
of rules and facts is required.
</p>

<p>
We can now extend this example a bit to show how <b><code>DLV</code></b>
can be used to model knowledge as datalog rules and exploit it.

First we add a few more facts to add more people and to express their gender:

<blockquote><pre>
parent(william, john).
parent(john, james).
parent(james, bill).
parent(sue, bill).
parent(james, carol).
parent(sue, carol).

male(john).
male(james).
female(sue).
male(bill).
female(carol).
</pre></blockquote>

Then we can add more rules that model family relationships.

<blockquote><pre>
grandparent(X, Y) :- parent(X, Z), parent(Z, Y).
father(X, Y) :- parent(X, Y), male(X).
mother(X, Y) :- parent(X, Y), female(X).
brother(X, Y) :- parent(P, X), parent(P, Y), male(X), X != Y.
sister(X, Y)  :- parent(P, X), parent(P, Y), female(X), X != Y.
</pre></blockquote>

The rules for brother and sister use <code>X != Y</code> to require that
X and Y are different (one cannot be his own brother). This is called a
built-in predicate, since it could be written as something like
<code>not_equal(X, Y)</code>. <b><code>DLV</code></b> knows quite a few of
these built-in predicates.
For this program, <b><code>DLV</code></b> finds the following model
(to simplify readability, the facts already listed above were removed from the
model below; of course, they still belong there):

<blockquote><pre>
{grandparent(william,james), grandparent(john,bill), grandparent(john,carol),
father(john,james), father(james,bill), father(james,carol),
mother(sue,bill), mother(sue,carol),
brother(bill,carol), sister(carol,bill)}
</pre></blockquote>

Let us now exchange the IDB rules against the following (the EDB facts remain
the same):

<blockquote><pre>
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
</pre></blockquote>

These rules are interesting, since they use recursion
to implement transitivity.
They express that, to start with, every parent is an ancestor, and, secondly,
that every parent of an ancestor is an ancestor.
Please note that the semantics used ensures that it is impossible that there
be any problems with left-recursion as they occur in languages as Prolog.
In <b><code>DLV</code></b>, the programmer can safely ignore such
considerations.
</p>

<p>
The model of this program combined with the six-entries <code>parent</code>
facts base above results in the following model (where the <code>parent</code>
facts were again removed for readability):

<blockquote><pre>
{ancestor(william,john), ancestor(william,james), ancestor(william,bill),
ancestor(william,carol), ancestor(john,james), ancestor(john,bill),
ancestor(john,carol), ancestor(james,bill), ancestor(james,carol),
ancestor(sue,bill), ancestor(sue,carol)}
</pre></blockquote>
</p>

<p>
Finally, some subtle detail has to be noted which is quite useful to improve
the readability of the rules. In the case that a certain argument of a
predicate is irrelevant for a certain rule, no dummy variable has to be
inserted, but the <code>_</code> can be used. For instance, suppose we want
to derive the persons from the parent facts. For this, we can write the
following rules:

<blockquote><pre>
person(X) :- parent(X, _).
person(X) :- parent(_, X).
</pre></blockquote>

<p>
Finally, please <em>avoid</em> calling a predicate as shown in this section a
proposition. (It is fine to call them atoms.)
</p>



<hr>
<h3>
<code>DLV</code> as a Deductive Database System; Comparison Operators
</h3>

<p>
When you use the CWA in one of your programs, you basically view the
<code>DLV</code> system as a <em>deductive</em> database system, since you
do not ask for what is logically right, but what you can usefully derive
from your facts base.
Following this approach, you can perform queries on the existing data (the
facts base), derive (and "store") new data using queries(=rules),
which again can be used to deduce even more data, and, using the CWA, even
ask queries as to what is <em>not</em> in (or derivable from) your database.
</p>

Consider the following example in SQL in the well know business domain (which
many relational database systems examples use). Emp is a relational table
containing employee information, and dept contains data on departmens of a
company in which the employees work.

<blockquote><pre>
SELECT e.name, e.salary, d.location
FROM   emp e, dept d
WHERE  e.dept = d.dept_id
AND    e.salary > 31000;
</pre></blockquote>

When the relational tables are encoded as a facts base, we can rewrite the
above query into a datalog rule:

<blockquote><pre>
emp("Jones",   30000, 35, "Accounting").
emp("Miller",  38000, 29, "Marketing").
emp("Koch",  2000000, 24, "IT").
emp("Nguyen",  35000, 42, "Marketing").
emp("Gruber",  32000, 39, "IT").

dept("IT",         "Atlanta").
dept("Marketing",  "New York").
dept("Accounting", "Los Angeles").

q1(Ename, Esalary, Dlocation) :- emp(Ename, Esalary, _, D), dept(D, Dlocation),
   Esalary > 31000.
</pre></blockquote>

<p>
As you can see, joins are achieved via variable binding (we use the same
variable D both in emp and in dept), selections can for example be achieved
by the comparison operators, and projections (i.e. where unwanted data columns
are excluded from a query result) can be accomplished by using _ or an
unbound variable.
</p>

<p>
You can use <code>DLV</code> to ask all the queries that are possible in the
core SQL language. Furthermore, (as you will see when the full expressive power
of <code>DLV</code> is unveiled later in this tutorial) you can also encode
many useful queries that cannot be expressed in SQL.
</p>

<p>
This example used another feature of <code>DLV</code> that has not been
introduced yet: comparison operators. <code>DLV</code> supports the operators
<, >, >=, <=, and = for integers, floating point values, and strings.
This is an extension that is not part of basic datalog, but it is convenient
and also compatible with the philosophy of datalog, as you can think of an
expression X > Y as a predicate
<code>greater_than(X,Y)</code> for which the facts base of all the greater-than
relationships between constant symbols in your program are automatically
generated.
Therefore, we call these comparison operators <em>built-in predicates</em>.
</p>

<p>
Note that you could also rewrite <code>q1</code> to use the operator = for the
join. The rule below obtains the same result as the one shown earlier:

<blockquote><pre>
q1(Ename, Esalary, Dlocation) :- emp(Ename, Esalary, _, D1),
                                 dept(D2, Dlocation), D1 = D2,
                                 Esalary > 31000.
</pre></blockquote>

<p>
<a href="examples/emp.dl">Download example program.</a>
</p>

</p>



<hr>
<h3>
The Railway Crossing Example : True Negation and Negation as Finite Failure
</h3>

<p>
<b><code>DLV</code></b> supports <em>two</em> kinds of negation.

Here, we emphasize the difference between explicitly expressing the falseness
of an atom and having it done by the <em>Complete World Assumption</em>.

The following program uses the CWA. It has the model
<code>{cross}</code> because train_approaching is assumed to be false (as it
being true is not stated anywhere).
This kind of negation is called
<em>negation as (finite) failure</em> or <em>naf</em>.
<blockquote><pre>
cross :- not train_approaching.
</pre></blockquote>

The next program uses so-called <em>true</em> or <em>classical negation</em>.
Since <code>-train_approaching</code> is not known to be true, the following
program has only an empty model.

<blockquote><pre>
cross :- -train_approaching.
</pre></blockquote>

The difference between the two kinds of negation is quite important:
In the first example, we cross the railroad track if we have no information
on any trains approaching, which is quite dangerous,
while in the second example, we only cross if we know for
sure that no train comes.
In particular, the left side of the previous rule will only be true if

<blockquote><pre>
-train_approaching.
</pre></blockquote>

is in the facts base of the program.
</p>

<p>
True negation is stronger than negation as finite failure. If something is
true via true negation, it is always also true if negated by negation as
finite failure.
For example, the program
</p>

<blockquote><pre>
cross :- not train_approaching.
-train_approaching.
</pre></blockquote>

has the model <code>{cross, -train_approaching}</code>.

<p>
Using True Negation also allows to build programs that are contradictory and
have no models. Consider the following example:

<blockquote><pre>
cross.
-cross.
</pre></blockquote>

Certainly, this program cannot have a model.
This is very different from a program that has an empty model, which would just
mean that the program represents a possible situation but that all of its atoms
are assumed to be false.
</p>



<hr>
<h3>
The Broken Arm Example : Disjunctive Datalog and the Stable Model Semantics
</h3>

Suppose you have met a friend recently and you know that he
had one of his arms broken, but you don't know which one.
Now you didn't receive a greeting card for your birthday and
wonder if you should be angry on him or if he just cannot
write because of his broken arm.
Finally, you know that he writes with his right hand.
The following <b>DLV</b> program computes the two possible
explanations for the observations you made.

<blockquote><pre>
left_arm_broken v right_arm_broken.
can_write :- left_arm_broken.
be_angry :- can_write.
</pre></blockquote>

The first rule is called a disjunctive rule; The <tt>v</tt> is read as "or"
and the whole rule is read as
"For sure, either the left or the right arm is broken."
As we can see here, a disjunctive rule may (but does not have to) have an
empty body (= lack a body).
It is still called a rule, since it is certainly not a fact.
(It is unknown if the left or the right arm is broken.)
<p>

Being able to process incomplete information (i.e. being unsure if the
left or the right arm is broken) is one of the great strengths of
<b><code>DLV</code></b>.

The resulting models of this query are
<code>{left_arm_broken, can_write, be_angry}</code> and
<code>{right_arm_broken}</code>.
<p>

In fact, the disjunction <code>left_arm_broken v right_arm_broken.</code>
also allows both <code>left_arm_broken</code> and <code>right_arm_broken</code>
to be true at the same time. Still, <b><code>DLV</code></b> does not output
the model <code>{left_arm_broken, right_arm_broken, can_write, be_angry}</code>
due to the computing paradigm that it uses to cope with uncertainty, and which
is called the <em>Stable Model Semantics</em>.
Under this semantics, a model is not stable if there is a smaller model which
is a subset of it (which is the case for both stable models shown
above with respect to the "big" model containing <code>left_arm_broken</code>
and <code>right_arm_broken</code>).
While this might seem complicated, it is a very powerful feature of
<b><code>DLV</code></b> which is very useful for all kinds of reasoning.
We will come back to this later in this tutorial.
(For the moment, we want to emphasize that this one "big" model which
is not stable would be obviously wrong in this application.)
<p>


Note that the same uncertainty can also be expressed by the following program:

<blockquote><pre>
left_arm_broken :- not right_arm_broken.
right_arm_broken :- not left_arm_broken.
can_write :- left_arm_broken.
be_angry :- can_write.
</pre></blockquote>

<p>
This program results in the same pair of models. The method used here is called
<em>Unstratified Negation</em> and is considered less elegant than the first
method. Also, there are certain interesting reasoning problems that
<b><code>DLV</code></b> can solve and which can only be expressed with true
disjunction but not with unstratified negation.
</p>

<p>
Finally, please note that rule bodies may either contain positive (nonnegated)
atoms, atoms negated by true negation, and atoms negated by negation as
failure, while rule heads may only contain positive atoms and true negation,
but no negation as failure. In other words, a rule such as

<blockquote><pre>
not a :- b.   % INVALID !!!
</pre></blockquote>

is <em>not</em> valid! (The % sign in a <b><code>DLV</code></b> program
starts a comment which goes to the right to the end of the line.)
</p>



<hr>
<h3>
Strong Constraints
</h3>

<p>
<b><code>DLV</code></b> also supports integrity constraints
(strong constraints).
A constraint is a rule with an empty head. If its body is true (which is of
course the case exactly if all the literals in the body are true at the same
time), a model is made inconsistent and is removed.

For example, in the family tree example which was presented earlier, we
can easily write an integrity constraint to assure that the facts base does not
erroneously contain contradicting facts saying that a person is male and
female at the same time.

<blockquote><pre>
:- male(X), female(X).
</pre></blockquote>

This kind of constraints is called <em>strong constraints</em> because there
is also a different kind (<em>weak constraints</em>) supported by
<b><code>DLV</code></b> which is not addressed in this tutorial.
This other kind of constraints is very useful to solve optimization problems.
</p>



<hr>
<h3>
Graph Coloring: Guess&Check Programming
</h3>

<p>
Graph 3-colorability is a hard (NP-complete) problem.
It is the problem of deciding if there exists a coloring of a map of
countries corresponding to the given graph using no more than three colors in
which no two neighbour countries (nodes connected by an arc) have the same
color.
It is known that every map can be colored given these constraints if four
colors are available.
</p>

<table><tr><td>
<img src="midwest2.gif">
</td><td>
<blockquote><pre>
node(minnesota).
node(wisconsin).
node(illinois).
node(iowa).
node(indiana).
node(michigan).
node(ohio).

arc(minnesota, wisconsin).
arc(illinois, iowa).
arc(illinois, michigan).
arc(illinois, wisconsin).
arc(illinois, indiana).
arc(indiana, ohio).
arc(michigan, indiana).
arc(michigan, ohio).
arc(michigan, wisconsin).
arc(minnesota, iowa).
arc(wisconsin, iowa).
arc(minnesota, michigan).
</pre></blockquote>
</td></tr></table>

This problem can now be solved with a very simple datalog program, in which
we first guess a coloring by using a disjunctive rule and then check it by
adding a (strong) constraint which deletes all those colorings that do not
satisfy our requirements (that there may be no arc between two nodes of
equal color):

<blockquote><pre>
% guess coloring
col(Country, red) v col(Country, green) v col(Country, blue) :- node(Country).

% check coloring
:- arc(Country1, Country2), col(Country1, CommonColor), col(Country2, CommonColor).
</pre></blockquote>

This problem instance has 6 solutions (stable models), therefore, it is
3-colorable. Below, one solution is shown, in which the facts base has again
be removed for better readability:

<blockquote><pre>
{col(minnesota,green), col(wisconsin,red), col(illinois,green),
 col(iowa,blue), col(indiana,red), col(michigan,blue), col(ohio,green)}
</pre></blockquote>

<p>
This method (guess&check programming) allows to encode a large number of
complicated problems in an intuitive way. <b><code>DLV</code></b> can then
use such an encoding to solve the problems surprisingly efficiently.
</p>

<p>
<a href="examples/3col.dl">Download example program.</a>
</p>

<p>
As an exercise, you can use <b><code>DLV</code></b> to prove that a
<a href="benelux.jpg">map of Germany, Belgium, Luxembourg and France</a>
is not 3-colorable.
</p>



<hr>
<h3>
The Fibonacci Example: Built-in Predicates and Integer Arithmetics
</h3>

Note that this section introduces some features of <b><code>DLV</code></b>
which are not part of standard datalog.
<p>

In the following example, the Fibonacci function is defined,
which is relevant in areas as disparate as Chaos Theory and Botanics.
Its starts with the following values:
1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, ...
(Apart from the first two values, each value is defined as the sum of the
previous two.)

<blockquote><pre>
true.
fibonacci(1, 1) :- true.
fibonacci(1, 2) :- true.
fibonacci(F, Index) :- +(F1, F2, F),
                       fibonacci(F1, Index1),
                       fibonacci(F2, Index2),
                       #succ(Index1, Index2),
                       #succ(Index2, Index).
</pre></blockquote>

This program uses the built-in predicates <code>+</code> (which adds or
subtracts integer numbers) and <code>#succ</code> (the successor function).
Note that for better readability, it is also correct to write
<code>F = F1 + F2</code> instead of <code>+(F1, F2, F)</code> and
<code>Index2 = Index1 + 1</code> instead of
<code>#succ(Index1, Index2)</code>.
Still, these simple equations always map to the built-in predicates and
may not be extended any further. (It is not allowed to write
<code>A = B + C + D</code>, this has to be split into two parts.)
<p>

<p>
The second topic that has to be discussed at this point is why the fact
<code>true.</code> was introduced.
The reason for this is the strong separation that is made between EDB and
IDB predicates. Since <code>fibonacci</code> is used on the left-hand side
of a rule, it is in the IDB. IDB predicates cannot be used in facts (because
then they would have to be in the EDB).
Because of that, a fact is introduced and rules are built that are always true
and are therefore equivalent to facts.

Note that this distinction between IDB and EDB predicates is not necessary
anymore in the most recent versions of <b><code>DLV</code></b>. Therefore,
you can now declare <code>fibonacci(1, 1)</code> and
<code>fibonacci(1, 2)</code> simply as facts.
</p>

<p>
Whenever integer arithmetics are used, the range of possible values has to
be restricted, since <b><code>DLV</code></b> requires the space of possible
solutions to be finite. This is done by invoking <b><code>DLV</code></b>
with the option <code>-N</code>. (For a full description of
<b><code>DLV</code></b> usage, refer to the
<a href="http://www.dlvsystem.com/man/">
<b><code>DLV</code></b> manual</a>.)

For example, invoking <b><code>DLV</code></b> with

<blockquote><pre>
dl -N=100 fibonacci.dl
</pre></blockquote>

results in the model

<blockquote><pre>
{true, fibonacci(1,1), fibonacci(1,2), fibonacci(2,3), fibonacci(3,4),
 fibonacci(5,5), fibonacci(8,6), fibonacci(13,7), fibonacci(21,8),
 fibonacci(34,9), fibonacci(55,10), fibonacci(89,11)}
</pre></blockquote>

These are all the Fibonacci numbers not greater than 100.
</p>

<p>
<a href="examples/fibonacci.dl">Download example program.</a>
</p>

<img src="fibSpiralANIM.gif">
<img src="fibspiral2.GIF">
<img src="shell.gif" width=84 height=120>

<br>
Click
<a href="http://www.mcs.surrey.ac.uk/Personal/R.Knott/Fibonacci/fib.html">here</a>
for some interesting material on Fibonacci numbers.



<hr>
<h3>
The 8-Queens Example: Guess&Check Programming with Integers
</h3>

The 8 queens problem asks for a solution in which 8 queens are placed on a
8 x 8 chess board without threatening eachother. A queen threatens another
if it is in the same row, column, or on a diagonal.

<blockquote><pre>
% guess horizontal position for each row
q(X,1) v q(X,2) v q(X,3) v q(X,4) v q(X,5) v q(X,6) v q(X, 7) v q(X,8) :- #int(X), X > 0.

% check

% assert that each column may only contain (at most) one queen
:- q(X1,Y), q(X2,Y), X1 <> X2.

% assert that no two queens are in a diagonal from top left to bottom right
:- q(X1,Y1), q(X2,Y2), X2=X1+N, Y2=Y1+N, N > 0.

% assert that no two queens are in a diagonal from top right to bottom left 
:- q(X1,Y1), q(X2,Y2), X2=X1+N, Y1=Y2+N, N > 0.
</pre></blockquote>

To run this program with <b><code>DLV</code></b>, type the following:

<blockquote><pre>
dl -n=1 -N=8 8queens.dl
</pre></blockquote>

This will return a result like

<blockquote><pre>
{q(1,3), q(2,7), q(3,2), q(4,8), q(5,5), q(6,1), q(7,4), q(8,6)}
</pre></blockquote>

To get all 92 correct solutions, type

<blockquote><pre>
dl -N=8 8queens.dl
</pre></blockquote>

<p>
<a href="examples/8queens.dl">Download example program.</a>
</p>



<hr>
<h3>
A simple Physics Diagnosis example
</h3>

We will now show how to use <b><code>DLV</code></b> to do diagnosis.
We choose a physics application domain, a simplified version of ECAL
pre-calibration.

<img src="h4.gif">
<br>

As shown in the picture, a test beam is directed onto a scintillating crystal
whose light emission is measured by an avalanche photodiode (APD).
The measurement is then read with some readout electronics.
Alternatively to the beam reading, the APD can receive a test pulse signal,
which allows to check the correct functioning of the APD independently from
the crystal.
The following program allows to automatically diagnose malfunctioning parts:

<blockquote><pre>
ok(testpulse_reading).
ok(beam_reading).

good(crystal) v bad(crystal).
good(apd) v bad(apd).

:- good(X), bad(X).

good(crystal) :- ok(beam_reading).
good(apd) :-     ok(beam_reading).
bad(apd) v bad(crystal) :- not ok(beam_reading).
good(apd) :-     ok(testpulse_reading).
bad(apd)  :- not ok(testpulse_reading).
</pre></blockquote>

The program starts with two facts expressing our observations.
Here, both the testpulse reading and the beam reading were found to be correct;
below, we will evaluate the program with different observations.
The following two rules tell the system that crystals and APDs are either
working or broken. After this follows a constraint that assures that they
cannot be both at the same time.

Finally, there are five rules that are a collection of expert knowledge.
They model the knowledge about the domain and show quite clearly why the
test pulse is available as a separate input to the APDs: it allows to
find out if the APD works correctly without having to make any assumptions
about the crystal.
If the reaout of the beam on the other hand were not correct, one could
not be sure if the responsible part is the crystal or the APD.
<p>

Here, the unique result is the model <code>{good(crystal), good(apd)}</code>.
Suppose we exchange the two EDB facts (the first two lines of this program)
to <code>ok(testpulse_reading).</code> then the result changes to
<code>{good(apd), bad(crystal)}</code>.
The whole set of different cases is shown in the following table:
<p>

<table border="1">
<tr>
<td><b>EDB</b></td>
<td><b>Model(s)</b></td>
</tr>

<tr>
<td> <code>{ok(testpulse_reading). ok(beam_reading).}</code> </td>
<td> <code>{good(crystal), good(apd)}</code> </td>
</tr>

<tr>
<td> <code>{ok(testpulse_reading).}</code> </td>
<td> <code>{good(apd), bad(crystal)}</code> </td>
</tr>

<tr>
<td> <code>{ok(beam_reading).}</code> </td>
<td> no model </td>
</tr>

<tr>
<td> <code>{}</code> </td>
<td> <code>{bad(apd), good(crystal)}, <br>
{bad(apd), bad(crystal)} </code> </td>
</tr>
</table>
<p>

The case that the facts base is <code>{ok(beam_reading).}</code>
is also interesting:
According to our program, if <code>ok(beam_reading)</code> is true,
<code>ok(testpulse_reading)</code> also has to be true.
Therefore, there is no consistent model in this case.
In other words, according to our program, such observations cannot be made.
<p>



<hr>
<h3>
A different way to implement the Physics Diagnosis example
</h3>

The way to do diagnosis that was presented in the previous section has two
drawbacks:
It requires that more knowledge than necessary has to be coded in the program,
and resulting from this, the program does not really do anything original.
Also, it it hard to extend.
Here, we show a different (better) way to do diagnosis in the same
application domain.
We represent the system as a graph of its units:

<blockquote><pre>
connected(beam, crystal).
connected(crystal, apd).
connected(testpulse_injector, apd).
connected(apd, readout).

good_path(X,Y) :- not bad(X), not bad(Y), connected(X, Y).
good_path(X,Z) :- good_path(X,Y), good_path(Y, Z).

bad(crystal) v bad(apd).

testpulse_readout_ok :- good_path(testpulse_injector, readout).
beam_readout_ok :- good_path(beam, readout).
</pre></blockquote>

In this example program, we have left away all the possible observations,
which we implement as constraints, as shown in the following table:
<p>

<table border="1">
<tr>
<td><b>Observations (Constraints)</b></td>
<td><b>Model(s) (good_path predicates omitted)</b></td>
</tr>

<tr>
<td> <code>{}</code> </td>
<td> <code>
{bad(crystal), testpulse_readout_ok},
<br>
{bad(apd)}
</code> </td>
</tr>

<tr>
<td> <code>{:- testpulse_readout_ok.}</code> </td>
<td> <code>{bad(apd)}</code> </td>
</tr>

<tr>
<td> <code>{:- beam_readout_ok.}</code> </td>
<td> <code>
{bad(crystal), testpulse_readout_ok},
<br>
{bad(apd)}
</code> </td>
</tr>

<tr>
<td> <code>{:- beam_readout_ok. <br> :- testpulse_readout_ok.}</code> </td>
<td> <code>{bad(apd)}</code> </td>
</tr>

<tr>
<td> <code>{:- not testpulse_readout_ok.}</code> </td>
<td> <code>
{bad(crystal), testpulse_readout_ok}
</code> </td>
</tr>

<tr>
<td> <code>{:- not beam_readout_ok.}</code> </td>
<td> no model </td>
</tr>

<tr>
<td> <code>{:- not beam_readout_ok. <br>
:- not testpulse_readout_ok.}</code> </td>
<td> no model </td>
</tr>

</table>
<p>

<a href="examples/diagnosis.dl">Download example program.</a>
<p>



<hr>
<h3>
The Monkey&Banana Example: Planning
</h3>

<p>
The following example shall give an idea of how <b><code>DLV</code></b>
can be used to do planning.
</p>

<p>
Please note that there is a <code>DLV</code> planning frontend
that uses a convenient special-purpose planning language and which is not
described in this tutorial. Instead, we use plain disjunctive datalog for
solving planning problems here.
If you are interested in this frontend, please refer to the
<a href="http://www.dlvsystem.com"><b><code>DLV</code></b>
homepage</a> for further information.
</p>

<p>
Consider the following classic planning problem.
A monkey is in a room with a chair and a banana which is fixed to the
ceiling.
The monkey cannot reach the banana unless it stands on the chair; it is simply
too high up. The chair is now at a position different from the place
where the banana is hung up, and the monkey itself initially is at again
a different place.
<p>

Since the program is quite long compared to the earlier examples, it will
be explained step by step.

<blockquote><pre>
walk(Time) v move_chair(Time) v ascend(Time) v idle(Time) :- #int(Time).
</pre></blockquote>

At each discrete point in time, the monkey performs one of the following
for actions: it walks, it moves the chair (while doing this, it also moves
through the room), it climbs up the chair, or it does nothing.
<tt>#int</tt> is again a built-in predicate which is true exactly if its
argument is an integer value.

<blockquote><pre>
monkey_motion(T) :- walk(T).
monkey_motion(T) :- move_chair(T).

stands_on_chair(T2) :- ascend(T), T2 = T + 1.
:- stands_on_chair(T), ascend(T).
:- stands_on_chair(T), monkey_motion(T).
stands_on_chair(T2) :- stands_on_chair(T), T2 = T + 1.
</pre></blockquote>

After climbing up the chair, it is on it. If is is already on it, it cannot
climb up any further. While on the chair, it cannot walk around.
If it was on the chair earlier, it will be there in the future.

<blockquote><pre>
chair_at_place(X, T2) :- chair_at_place(X, T1), T2 = T1 + 1, not move_chair(T1).
chair_at_place(Pos, T2) :- move_chair(T1), T2 = T1 + 1,
   monkey_at_place(Pos, T2).
</pre></blockquote>

If the chair is not moved, it will stay at the same place.
If the monkey moves the chair, it changes its position.

<blockquote><pre>
monkey_at_place(monkey_starting_point, T) v
monkey_at_place(chair_starting_point, T) v
monkey_at_place(below_banana, T) :- #int(T).
</pre></blockquote>

The monkey is somewhere in the room. (For simplicity, only three positions are
possible.)

<blockquote><pre>
:- monkey_at_place(Pos1, T2), monkey_at_place(Pos2, T1),
   T2 = T1 + 1, Pos1 != Pos2, not monkey_motion(T1).

:- monkey_at_place(Pos, T2), monkey_at_place(Pos, T1), T2 = T1 + 1,
   monkey_motion(T1).

:- ascend(T), monkey_at_place(Pos1, T), chair_at_place(Pos2, T), Pos1 != Pos2.

:- move_chair(T), monkey_at_place(Pos1, T), chair_at_place(Pos2, T),
   Pos1 != Pos2.
</pre></blockquote>

The monkey cannot change its position without moving.
The monkey cannot stay at the same place if it moves.
It cannot climb up the chair if it is somewhere else.
It cannot move the chair if it is somewhere else.

<blockquote><pre>
monkey_at_place(monkey_starting_point, 0) :- true.
chair_at_place(chair_starting_point, 0) :- true.
true.
</pre></blockquote>

Initially, the monkey and the chair are at different positions.

<blockquote><pre>
can_reach_banana :- stands_on_chair(T), chair_at_place(below_banana, T).
eats_banana :- can_reach_banana.
happy :- eats_banana.

:- not happy.
</pre></blockquote>

The monkey can only reach the banana if it stands on the chair and the
chair is below the banana.
If it can reach the banana, it will eat it, and this will make it happy.
Our goal is to make the monkey happy.

<blockquote><pre>
step(N, walk, Destination) :- walk(N), monkey_at_place(Destination, N2),
                              N2 = N + 1.
step(N, move_chair, Destination) :- move_chair(N),
                                    monkey_at_place(Destination, N2),
                                    N2 = N + 1.
step(N, ascend, " ") :- ascend(N).
</pre></blockquote>
<! %step(N, idle, " ") :- idle(N).>

The step rules collect all the things we can derive from the situation and
build a consistent plan. (There is no step rule for the action <tt>idle</tt>
since we are not interested in it.)
<p>

This program again uses integer arithmetics; to find a plan, the maximum
integer variable has to be set to at least 3:

<blockquote><pre>
dl -N=3 banana.dl
</pre></blockquote>

This results in the following model (If N is set to a value greater than 3,
<b><code>DLV</code></b> will find other plans that make the monkey happy.)

<blockquote><pre>
{chair_at_place(chair_starting_point,0),
monkey_at_place(monkey_starting_point,0),
monkey_at_place(chair_starting_point,1),
monkey_at_place(below_banana,2),
monkey_at_place(below_banana,3),
walk(0), move_chair(1), ascend(2), idle(3),
chair_at_place(chair_starting_point,1),
chair_at_place(below_banana,2),
chair_at_place(below_banana,3),
monkey_motion(0), monkey_motion(1),
step(0,walk,chair_starting_point),
step(1,move_chair,below_banana),
step(2,ascend," "),
stands_on_chair(3), can_reach_banana, eats_banana, happy}
</pre></blockquote>

<a href="examples/banana.dl">Download example program.</a>
<p>



<hr>


<!/font>
</body>

</html>