はじめに

Vladimir Lifschitz氏によるAnswer Set Programming (Draft) (リンク)の第1章第2章の要約です。輪講に利用したものをほぼそのまま流用しているので、表記がおかしかったらごめんなさい。

Clingoについて

HomebrewであればこれでOKです。

% brew install clingo

そのほかの方法はここにありますが、試していないのでやってみてください。
また、clingoのドキュメンテーションはここです。

large(C) :- size(C,S1), size(uk,S2), S1 > S2.

意味は「Cの大きさがS1かつukの大きさはS2かつS1 > S2ならばCは大きい」
large(C)はhead(頭部)
size(C,S1), size(uk,S2), S1 > S2はbody(本体)
- :-がないルールは、bodyがないルールとして扱う。
large(C),size(C,S1),size(uk,S2)はatom
- 関係や性質を表すpredicate(述語) symbolとカッコ内の引数のリスト（任意）からなる
- コンマで区切られた表現は、論理積$\wedge$と同じ
S1>S2はcomparison
- =, !=, <, >, <=, >=のいずれかのシンボルと、その両側の二つの引数からなる
引数になる表現をtermと呼ぶ
- Symbolic constraint - 小文字から始まる文字、数字、アンダ-スコアの文字列
- Numeric constraint - 10進数の整数
- Variables - 大文字から始まる文字、数字、アンダースコアの文字列
- 複雑なtermは後述
Atomやruleなどの内、variableがないものをgroundであるといい、「事実」を示す
- ex) size(uk,64).

large(C) :- size(C,S1), size(uk,S2), S1 > S2.
size(uk,64).  size(france,65).

large(france)がstable modelに含まれるのは、C,S1,S2をそれぞれfrance, 65, 64に置き換えた

large(france) :- size(france,65), size(uk,64), 65 > 64.

が存在するからである

p(X) :- X > 7.のような無限にstable modelが存在するようなルールは”unsafe variable”のエラーで実行できない
size(uk,64). size(france,65).は
size(france,65; uk,64).のように省略して書くことができる (pooling)

#show p/2.
- predicate symbolがpで引数が2のもの以外を表示しない
  - clingoでは、同じpredicates symbolでも引数の数が異なれば別の述語として扱う
#const c0=uk.
- symbolic constraint c0を定数ukに置き換える
- コマンドラインオプション -c c0=ukも同じ
#include “large_input.lp”.
- 他のファイルを連結する
- コマンドから% clingo large.lp large_input.lpも同じ
%から行末まではコメント

多くのルールは定義として見ることができる
- ex) grandparent/2はparent/2を使って次のように表現できる
```
  grandparent(X, Z) :- parent(X, Y), parent(Y, Z)
```

predicateは複数の定義から成ることもある

parent(X, Y) :- mother(X, Y).
parent(X, Y) :- father(X, Y).

predicateは再帰的に定義することができる

ancestor(X, Y) :- parent(X, Y).
ancestor(X, Z) :- ancestor(X, Y), ancestor(Y, Z).

1ステップで定義できないこともある

composite(N) :- N= 1..5, I = 2..N-1, N\I=0.
prime(N) :- N=2..5, not composite(N).

notはnegation as failureを示す
- 導出できない時に真になる
- 言い換えれば、明示的に述語を否定することによって真になるわけではないということでもある。

ASPでは複数のstable modelが存在するものを扱うことが多い
{p(a); q(b)}.はp(a), q(b)がそれぞれ含まれるかを選んだ全ての通りのモデルを表すルールである
- このルールだけの場合、stable modelは$\phi$, p(a), q(b), p(a)q(b)の4通り
- 全てのstable modelを見るためには% clingo choice.lp 0で実行
poolingとintervalを利用することもできる
- {p(1;2;3)}.と{p(1..3)}.は{p(1); p(2); p(3)}.と同じ
モデルに含まれる要素の数の上限と下限を1 {p(1..3)} 2.のように定義できる
- このルールのみのstable modelはp(1), p(2), p(3), p(1)p(2), p(1)p(3), p(2)p(3)
- 下限や上限のみを指定することもできる
- 下限と上限が等しい時{p(1..3)}=2.のように書ける

Choice ruleのbodyには変数を含めることもできる(Global variables)
- {p(X); q(X)} = 1 :- X=1..2.はp(1)かq(1)のいずれかと、p(2)とq(2)のいずれかを安定モデルに含む
- {p(1); q(1)} = 1. {p(2); q(2)} = 1.と同じ
Local variables はChoice ruleのカッコ内のatomを、すでに定義されているpredicateで定義したい時に利用できる
- person/1が定義されている時、{elected(X) : person(X)} = 3.でstable modelは当選した人が3人のみになる
- person(ann; bob; carol; dan; elaine; fred)ならば、上の式は
  {elected(ann; bob; carol; dan; elaine; fred)} = 3 と同じ

Headがないルールはconstraintであり、bodyを満たすmodelはstable modelとならないという制約を示す
- :- p(1). の時、stable modelはp(1)を含まない
- :- not p(1). の時、stable modelは必ずp(1)を含む
- :- p(1), p(2).の時、p(1)とp(2)を両方含むmodelはstable modelにならない
constraintは変数を含むことができる
- :- p(X), q(X).はp/1とq/1が互いに素であることを示す（p/1とq/1を同時に満たす要素が存在しないstable modelを排除する)
comparisonを含むこともできる
- :- f(X, Y1), f(X, Y2), Y1 != Y2.はf/2が関数であることを示す
- constraintのbodyのcomparisonは、headの逆のcomparisonに置き換えることができる
  - ex) Y1 = Y2 :- f(X, Y1), f(X, Y2).

filled/3はfilled(R, C, X)が行R列Cに値Xが入っている表を表すとする。
R1 = R2 :- filled(R1, C1, X), filled(R2, C2, X).は同じ値は同じ行にしか入らないことを示している。
- C1,C2は一度しか使われていない
上記のような一度しか登場しない変数はアンダースコアに置き換えることができる
R1 = R2 :- filled(R1, _, X), filled(R2, _, X).
内部的には補助的な述語に置換されている
```
R1 = R2 :- aux(R1, X), aux(R2, X).
aux :- filled(R, Var, X).
```
- aux/2は結果には表示されない
この処理方法は特に否定が利用される場合に重要である
- {p(1..2)} :- not p(Var).はVarについてunsafeとしてエラーとなる
- {p(1..2)} :- not p(_).は以下に置換されて、p(1), p(2), p(1)p(2)のstable modelが出力される
```
  {p(1..2)}.
  aux :- p(Var).
  :- not aux.
```

clingoのタグください。