Content deleted Content added
Bluelink 1 book for verifiability. [goog]) #IABot (v2.0) (GreenC bot |
m Task 70: Update syntaxhighlight tags - remove use of deprecated <source> tags |
||
Line 22:
An AnsProlog program consists of rules of the form
<
<head> :- <body> .
</syntaxhighlight>
The symbol <code>:-</code> ("if") is dropped if <code><body></code> is empty; such rules are called ''facts''. The simplest kind of Lparse rules are [[Stable model semantics#Programs with constraints|rules with constraints]].
Line 30:
One other useful construct included in this language is ''choice''. For instance, the choice rule
<
{p,q,r}.
</syntaxhighlight>
says: choose arbitrarily which of the atoms <math>p,q,r</math> to include in the stable model. The lparse program that contains this choice rule and no other rules has 8 stable models—arbitrary subsets of <math>\{p,q,r\}</math>. The definition of a stable model was generalized to programs with choice rules.<ref>{{cite book |first1=I. |last1=Niemelä |first2=P. |last2=Simons |first3=T. |last3=Soinenen |chapter=Stable model semantics of weight constraint rules |editor1-first=Michael |editor1-last=Gelfond |editor2-first=Nicole |editor2-last=Leone |editor3-first=Gerald |editor3-last=Pfeifer |title=Logic Programming and Nonmonotonic Reasoning: 5th International Conference, LPNMR '99, El Paso, Texas, USA, December 2–4, 1999 Proceedings |chapterurl=https://books.google.com/books?id=Abj-OpFeDjQC&pg=PA317 |year=2000 |publisher=Springer |isbn=978-3-540-66749-0 |pages=317–331 |series=Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence |volume=1730}} [http://www.tcs.hut.fi/~ini/papers/nss-lpnmr99-www.ps.gz as Postscript]</ref> Choice rules can be treated also as abbreviations for [[Stable model semantics#Stable models of a set of propositional formulas|propositional formulas under the stable model semantics]].<ref>{{cite journal |first1=P. |last1=Ferraris |first2=V. |last2=Lifschitz |title=Weight constraints as nested expressions |journal=Theory and Practice of Logic Programming |volume=5 |issue=1–2 |pages=45–74 |date=January 2005 |doi=10.1017/S1471068403001923 |arxiv=cs/0312045 }} [http://www.cs.utexas.edu/users/vl/papers/weight.ps as Postscript]</ref> For instance, the choice rule above can be viewed as shorthand for the conjunction of three "[[excluded middle]]" formulas:
Line 40:
The language of lparse allows us also to write "constrained" choice rules, such as
<
1{p,q,r}2.
</syntaxhighlight>
This rule says: choose at least 1 of the atoms <math>p,q,r</math>, but not more than 2. The meaning of this rule under the stable model semantics is represented by the [[propositional formula]]
Line 52:
Cardinality bounds can be used in the body of a rule as well, for instance:
<
:- 2{p,q,r}.
</syntaxhighlight>
Adding this constraint to an Lparse program eliminates the stable models that contain at least 2 of the atoms <math>p,q,r</math>. The meaning of this rule can be represented by the propositional formula
Line 62:
Variables (capitalized, as in [[Prolog#Data types|Prolog]]) are used in Lparse to abbreviate collections of rules that follow the same pattern, and also to abbreviate collections of atoms within the same rule. For instance, the Lparse program
<
p(a). p(b). p(c).
q(X) :- p(X), X!=a.
</syntaxhighlight>
has the same meaning as
<
p(a). p(b). p(c).
q(b). q(c).
</syntaxhighlight>
The program
<
p(a). p(b). p(c).
{q(X):-p(X)}2.
</syntaxhighlight>
is shorthand for
<
p(a). p(b). p(c).
{q(a),q(b),q(c)}2.
</syntaxhighlight>
A ''range'' is of the form:
<
(start..end)
</syntaxhighlight>
where start and end are constant valued arithmetic expressions. A range is a notational shortcut that is mainly used to define numerical domains in
a compatible way. For example, the fact
<
a(1..3).
</syntaxhighlight>
is a shortcut for
<
a(1). a(2). a(3).
</syntaxhighlight>
Ranges can also be used in rule bodies with the same semantics.
Line 109:
A ''conditional literal'' is of the form:
<
p(X):q(X)
</syntaxhighlight>
If the extension of q is {q(a1); q(a2); ... ; q(aN)}, the above condition is semantically equivalent to writing p(a1), p(a2), ... , p(aN) in the place of the condition. For example,
<
q(1..2).
a :- 1 {p(X):q(X)}.
</syntaxhighlight>
is a shorthand for
<
q(1). q(2).
a :- 1 {p(1), p(2)}.
</syntaxhighlight>
==Generating stable models==
To find a stable model of the Lparse program stored in file <code>${filename}</code> we use the command
<
% lparse ${filename} | smodels
</syntaxhighlight>
Option 0 instructs smodels to find ''all'' stable models of the program. For instance, if file <code>test</code> contains the rules
<
1{p,q,r}2.
s :- not p.
</syntaxhighlight>
then the command produces the output
<
% lparse test | smodels 0
Answer: 1
Line 157:
Answer: 6
Stable Model: r q s
</syntaxhighlight>
==Examples of ASP programs==
Line 166:
This can be accomplished using the following Lparse program:
<
c(1..n).
1 {color(X,I) : c(I)} 1 :- v(X).
:- color(X,I), color(Y,I), e(X,Y), c(I).
</syntaxhighlight>
Line 1 defines the numbers <math>1,\dots,n</math> to be colors. According to the choice rule in Line 2, a unique color <math>i</math> should be assigned to each vertex <math>x</math>. The constraint in Line 3 prohibits assigning the same color to vertices <math>x</math> and <math>y</math> if there is an edge connecting them.
Line 176:
If we combine this file with a definition of <math>G</math>, such as
<
v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .
</syntaxhighlight>
and run smodels on it, with the numeric value of <math>n</math> specified on the command line, then the atoms of the form <math>\mathrm{color}(\dots,\dots)</math> in the output of smodels will represent an <math>n</math>-coloring of <math>G</math>.
Line 189:
A [[Clique (graph theory)|clique]] in a graph is a set of pairwise adjacent vertices. The following lparse program finds a clique of size <math>\geq n</math> in a given graph, or determines that it does not exist:
<
n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).
</syntaxhighlight>
This is another example of the generate-and-test organization. The choice rule in Line 1 "generates" all sets consisting of <math>\geq n</math> vertices. The constraint in Line 2 "weeds out" the sets that are not cliques.
Line 199:
A [[Hamiltonian cycle]] in a [[directed graph]] is a [[Path (graph theory)|cycle]] that passes through each vertex of the graph exactly once. The following Lparse program can be used to find a Hamiltonian cycle in a given directed graph if it exists; we assume that 0 is one of the vertices.
<
{in(X,Y)} :- e(X,Y).
Line 209:
:- not r(X), v(X).
</syntaxhighlight>
The choice rule in Line 1 "generates" all subsets of the set of edges. The three constraints "weed out" the subsets that are not Hamiltonian cycles. The last of them uses the auxiliary predicate <math>r(x)</math> ("<math>x</math> is reachable from 0") to prohibit the vertices that do not satisfy this condition. This predicate is defined recursively in Lines 4 and 5.
Line 221:
The computed structure is a linearly ordered rooted tree.
<
% ********** input sentence **********
word(1, puella). word(2, pulchra). word(3, in). word(4, villa). word(5, linguam). word(6, latinam). word(7, discit).
Line 250:
:- root(X), node(Y, _), X != Y, not path(X, Y).
leaf(X) :- node(X, _), not arc(X, _, _).
</syntaxhighlight>
== Language standardization and ASP Competition ==
| |||