原著: https://github.com/potassco/guide/releases/download/v2.2.0/guide.pdf

ライセンス: This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License. http://creativecommons.org/licenses/by-sa/4.0

ほぼ自動翻訳によるもので内容は正確ではありません。正確な情報は原著を参照してください。

まだほんの最初の方しか翻訳できてません。続きを翻訳する予定も今のところありません。

概要

本書は、ポツダム大学で開発されたアンサーセット・プログラミング（ASP）ツールのgringo、clasp、clingoについて紹介しています。ASPの基本的な考え方は、問題を論理プログラムの形で表現し、その論理モデル（アンサーセットと呼ばれる）が元の問題の解決策を提供するというものです。最初のツールであるgringoは、ユーザーが提供した（変数を含む）論理プログラムを、等価な（変数を含まない）命題論理プログラムに変換する、いわゆるグラウンダーです。2番目のツールであるclaspは、gringoによって発行された命題プログラムの答えのセットを計算する、いわゆるソルバーです。3つ目のツールであるclingoは、gringoとclaspの機能を組み合わせたもので、さらにスクリプト言語であるLuaとPythonをライブラリや埋め込みコードで統合しています。このガイドは、ASPの初心者が上述のツールを利用できるようにすることを目的としています。もう一つは、ASPの熟練者が利用したくなるようなツールの機能を紹介しています。

これは、Potasscoガイドのバージョン2.2.0で、asprin 3.1とclingo[DL] 1.0のシステム、およびcondaパッケージ管理システムによるpotasscoソフトウェアのインストールについて説明しています。バージョン2.1.0では、すべてのコードをclingoシリーズ5にアップグレードし、セクション11.2ではasprin 3.0について説明しています。
対応する（またはそれ以降の）バージョンが利用可能であることを確認してください。

このドキュメントには、多くの例題が含まれています。
これらの例題は、ファイル名をクリックしてディスクに保存することができます。ビューアによっては、右クリックまたはダブルクリックで保存されます。

1 Introduction

Potsdam Answer Set Solving Collection (Potassco; [28, 33, 74]) は，アンサーセット・プログラミング (ASP; [3, 7, 12, 48, 49, 50, 63, 68, 70]) のためのさまざまなツールを集めたもので， grounder gringo，solver clasp，およびそれらを統合した ASP システム clingo が含まれる．これらの共通の目標は、ユーザーが、論理プログラムとその解答セットに基づく宣言型プログラミングパラダイムであるASPで、計算上困難な問題を迅速に解決できるようにすることです。

このガイドは、ASPの初心者が前述のツールを利用できるようにすることを目的としています。もう1つは、ASPの熟練者が利用したくなるようなツールの機能のリファレンスを提供することです。gringo（およびclingo）の入力言語とその正確なセマンティクスの正式な紹介は、[26]に記載されています（大きな断片）。gringoとclaspで使用されている接地と解法の技術の基礎とアルゴリズムは、[33]で詳細に説明されています。ASPの詳細については、文献[7, 49]を参照されたい。

実際、このガイドではASPに焦点を当て、論理プログラムの解答セットを計算することを目的としている[51]。さらに、claspは本格的なSAT、MaxSAT、PBソルバーとして使用でき（[9]参照）、DIMACS形式（拡張）の命題付きCNF式や、OPB、WBO形式のPB式を受け入れることができる。

1.1 Download and Installation

Potassco社のツールであるgringo，clasp，clingoは，C++で記述されており，MIT License [1]の下で公開されています．ソースパッケージおよびLinux，MacOS，Windows用のコンパイル済みバイナリは，[74]から入手できます．ソースからツールをビルドする場合は，最新のソースパッケージをダウンロードし，同梱のREADMEファイルを参照し，ビルドするマシンに必要なソフトウェアがすべてインストールされていることを確認してください．ビルドの過程で問題が発生した場合は、[74]のサポートページを参照するか、Potasscoのメーリングリスト（potassco-users@lists.sourceforge.net）をご利用ください。

最新のPython対応clingoバージョンを含むpotasscoソフトウェアを簡単にインストールするには、パッケージ管理システムconda [17]を使用することをお勧めします。

軽量のminicondaか、やや大型のanacondaのいずれかをインストールします。
ディストリビューションをインストールします。後者は、パッケージマネージャのグラフィカルなフロントエンドのような追加パッケージをデフォルトで配布しています。パッケージマネージャのグラフィカルなフロントエンドのような追加パッケージをデフォルトで同梱しています。インストール方法は、https://conda.io/docs/user-guide/install/ のインストール手順に従ってください。index.htmlに記載されているインストール手順に従うだけで、どちらもインストールできます。
次に、https://conda.io/docs/ にあるcondaのスタートガイドに従います。 user-guide/getting-started.html に掲載されているcondaの入門ガイドに従って、環境の作成やパッケージの管理方法を学びます。
この時点で、clingoはpotasscoチャンネルからインストールすることができます。コマンドラインインターフェースを使用している場合は、conda install -c potassco clingoと実行してください。その他のパッケージについては、https://anaconda.org/potassco をご覧ください。

ツールをインストールする別の方法として、パッケージマネージャを使用する方法があります。現在、Debian、Ubuntu、Arch Linux（AUR）、およびMacOS X（HomebrewまたはMacPorts）用のパッケージとポートがあります。なお，この方法でインストールされたパッケージは，常に最新の状態にあるわけではありません。

その後、ツールをﬂag—version(バージョン情報の取得)またはﬂag—help(利用可能なコマンドラインオプションの確認)で起動することで、すべてが正常に動作しているかどうかを確認することができます。例えば、gringoというバイナリがパスに含まれていると仮定すると（他のツールも同様）、以下の2つのコマンドを実行できます。

gringo --version
gringo --help

gringo、clasp、clingoは、コマンドライン（Linuxシェル、Winowsのコマンドプロンプトなど）で動作することに注意してください。これらを起動するには、バイナリをシステムパスのどこかのディレクトリに置くだけでインストールできます。呼び出しの際には、gringoやclingoの引数として、入力（テキスト）ファイルのファイル名を与えるのが一般的で、gringoの出力はclaspにパイプされるのが一般的です。このように、標準的なinvocationスキームは以下の通りです。

gringo [ options | files ] | clasp [ options | number ]
clingo [ options | files | number ]

clasp または clingo のいずれかに与えられる数値引数は、計算するアンサー集合の最大数を決定します。デフォルトでは、（存在する場合）1つのアンサー集合のみが計算されます。

1.2 Outline

このガイドでは、gringo、clasp、clingoの使い方の基本を紹介しています。特に、難解な計算問題の「解決までの時間」を大幅に短縮することで、読者がこれらを活用できるようにすることを目的としています。この目的のため、セクション2では、論理プログラムを用いた問題モデリングのプロトタイプとして、またgringoのモデリング言語のappetizerとしての役割を果たす入門的な例題を提供しています。セクション3では、我々のツールの入力言語について説明する。セクション3.1では、gringoとclingoの連結入力言語について詳細に説明し、一方、claspがサポートするソルバーフォーマットは、ユーザが直接記述することを想定しておらず、セクション3.2で簡単に説明している。セクション3.2では、clingoがサポートするソルバーのフォーマットについて説明し、セクション4では、マルチショットソルバーに必要なclingoの制御能力について説明します。さらに、セクション6では、よく知られている3つの例題を、我々のツールでどのように解決できるかを説明します。また、セクション7と8では、実用的な側面に焦点を当て、利用可能なコマンドラインオプションや、入力関連のエラーや警告について詳しく説明し、ヒントを示しています。次のセクションでは、基本的なモデリング言語と制御能力の高度な拡張について説明します。特に、セクション9では、ASPを用いて論理プログラムを再解釈することができるメタプログラミング機能について説明します。セクション10では、ASPの解決プロセスにドメイン固有のヒューリスティクスを組み込む技術を紹介します。セクション11では、プリファレンス処理と最適化のための高度な手法を紹介します。さらに、セクション5.3では、多値の変数や量的制約を扱うために開発された概念を提供しています。さらに、セクション12では、効率性を高めるために、ソルバーの設定に関する原理的なアプローチを紹介します。最後に、セクション13でまとめを行います。

gringo3 シリーズに慣れている読者のために、付録 B には現在のシリーズとの最も顕著な違いが記載されています。そうでなくても、gringoおよびclingoシリーズ4は、gringo3(および主要なグラウンダーであるlparse[80] 1) が認識するほとんどの入力を受け入れるはずです．ソルバーclaspの入力は、gringoのすべてのバージョン(およびlparse)で生成できます。シリーズ3の言語とシリーズ4の言語の間には、いくつかの構文上および意味上の変更があるので、すでにあるエンコーディングをシリーズ4で使用するために適応させなければならないことに注意してください。このドキュメントでは、例を挙げて説明しています。これらの例の多くは、実際に実行することができます。右のようなマージンボックスには、その方法が書かれています（場合によってはmeta-remarksも）。また、「\」という表記は、スペースの関係で改行されているコマンドラインのテキストが、実際には連続していることを意味します。

前置きが長くなりましたが、いよいよPotassco[74]の主要なツールを使ったガイドツアーを開始します。楽しくて役に立つ内容になっていることを期待しています。

2 Quickstart

ここでは，3本のペグと大きさの異なる4つの円盤からなる，簡単なハノイの塔のパズルを考えてみましょう．図1に示すように，目的は，すべての円盤を左のペグから右のペグに移動させることであるが，一度に移動できるのは，ペグの一番上の円盤だけである．さらに、すでに小さいディスクがあるペグにディスクを移動することはできない。この単純なハノイの塔のパズルを解くための効率的なアルゴリズムが存在するが、我々はそれを利用せず、以下では単に一連の動きが解となるための条件を示している。

ASPでは，統一的な問題定義を行うことが習慣となっている[68, 70, 77]．この方法論に従って、次の問題のインスタンスとエンコーディング（すべてのインスタンスに適用）を別々に指定する：ディスクの初期配置、ゴールの状況、数nが与えられたとき、ゴールを達成するn個の動きのシーケンスがあるかどうかを決定する。この問題は、ASPでエレガントに記述でき、gringoやclaspのようなドメインに依存しないツールで解決できることがわかります。このような宣言的な解決策を今から例示する。

2.1 Problem Instance

ハノイの塔のパズルのペグとディスクを、peg/1とdisk/1(数字は述語のアリティ(引数の数)を表す)という述語上のファクトで記述する。円盤は、1から始まる連続した整数で番号付けされ、小さい番号の円盤は、大きい番号の円盤よりも大きいとみなされる。さらに、init_on/2とgoal_on/2という述語は、それぞれ、初期状態とゴール状態を表す。それらの引数であるディスクの番号とペグの名前は、それぞれの状況におけるディスクの位置を決定する。最後に、moves/1という述語は、ゴールが達成されなければならない手の数を指定します。図1のハノイの塔のパズルは、15手の場合、次のようになります。

toh_ins.lp

peg(a;b;c).
disk(1..4).
init_on(1..4,a).
goal_on(1..4,c).
moves(15).

1行目の;は、文をpeg(a).、peg(b).、peg(c)という3つの事実に展開するための構文糖(セクション3.1.10で詳述)であることに注意してください。同様に、2-4行目で使用されている1..4は、間隔を意味します(3.1.9項で詳述)。ここでは、4つの値の異なる事実を省略しています。1、2、3、4。要約すると、1-5行目の事実は、図1のハノイの塔のパズルと、15手以内にゴールを達成すべきだという要件を表しています。

2.2 Problem Encoding

ここでは、「ハノイの塔」をschematicルールで表現します。すなわち，特定のインスタンスに依存しない変数(変数名は大文字で始まる)を含むルールである。
一般的に、エンコーディングは論理的にGenerate, Deﬁne, Testの各パートに分割される[63]。
追加のDisplayパートは、出力をアトムの識別セットに制限することができ、したがって、補助的な述語を抑制することができる。我々はこの方法論に従い、以下のエンコーディングで%で始まるコメント行で各パートをマークする。

toh_enc.lp

% Generate
% movesがM回で、T手目にdisk:Dをpeg:Pへ移すのは１通り
{ move(D,P,T) : disk(D), peg(P) } = 1 :- moves(M), T = 1..M.

% Define
move(D,T) :- move(D,_,T).
on(D,P,0) :- init_on(D,P).
on(D,P,T) :- move(D,P,T).
on(D,P,T+1) :- on(D,P,T), not move(D,T+1), not moves(T).
blocked(D-1,P,T+1) :- on(D,P,T), not moves(T).
blocked(D-1,P,T) :- blocked(D,P,T), disk(D).

% Test
:- move(D,P,T), blocked(D-1,P,T).
:- move(D,T), on(D,P,T-1), blocked(D,P,T).
:- goal_on(D,P), not on(D,P,M), moves(M).
:- { on(D,P,T) } != 1, disk(D), moves(M), T = 1..M.

% Display
#show move/3.

なお、変数D、P、T、Mは、それぞれ円盤、ペグ、手数、一連の動きの長さを表すのに使われています。

解答の候補を記述するGenerate部分は、2行目のルールで構成されています。これは、回数の各時点T(0以外)において、ディスクDのあるペグPへの移動を正確に1回実行しなければならないことを表しています。ルールの頭(:-の左)は、いわゆるカーディナリティ制約です(セクション3.1.12参照)。これは、コロンの後ろの条件(セクション3.1.11で詳述)を使って展開されたリテラルのセットと、ガード=1で構成されています。カーディナリティ制約は、ガードで指定されたとおり、真の要素の数が1に等しい場合に満たされます。カーディナリティ制約はルールの先頭にあるので、move/3が真であるという述語の上のアトムを導き出す(「推測する」)ことができます。本文(:-の右)では、(セクション3.1.8で詳しく説明しますが)T = 1..Mを、1から最大時点Mまでの各時点Tを指すように定義しています。ここまでは、大きな円盤を小さな円盤の上に移動させてはいけない、などの条件を付けていません。

4-9行目のDeﬁne部分には、補助的な述語、つまり、手元にある解答候補のプロパティを提供する述語を定義するルールが含まれている。(4行目のルールは、単純にディスクとタイムポイントにムーブを投影しています。結果として得られる述語move/2は、対象となるペグがinsigniﬁcantであるときはいつでも使用することができるので、そのアトムの1つは実際に3つの可能なケースを包含します。さらに、on/3という述語は、各時点でのハノイの塔パズルの状態を捉えます。このため、5行目のルールでは、タイムポイント0でのディスクの位置を初期状態(インスタンスで与えられる)と同一視しています。状態の遷移は6行目と7行目のルールでモデル化されています。前者は時点Tでの移動の直接的な効果、すなわち影響を受けたディスクDがターゲットペグPに再配置されることを指定していますが、後者はinertiaを記述しています。すなわち、ディスクDの位置は、T+1でDが移動されなければ、時点TからT+1に引き継がれます。7行目のnot moves(T)の使い方を見てください。これは、最大時点を超えてディスクの位置を導き出すことを防ぐものです。最後に、補助述語blocked/3を定義して、D-1より大きい数の小さいディスクがペグPに配置されていることを示す。8行目のルールは、Tが最大時点でないことを条件に、on(D,P,T)から時点T+1のこの条件を導き出す。9行目のルールは、ブロックされているという状態を、同じペグ上のすべての大きなディスクにさらに伝播させる。なお、どのディスクも参照していないD-1=0もブロックされているとマークしているが、これは次のテスト部分で冗長な動きを排除するのに便利である。

Test部分は、11-14行目の整合性制約で構成され、意図しない解の候補を排除するルールです。最初の11行目の整合性制約は、D-1が時点Tでブロックされている場合、ディスクDをペグPに移動させてはならないことを主張している。これは、大きなディスクを小さなディスクの上に置く動きを除外し、blocked/3の定義を考慮して、ディスクを以前の位置に戻すことも除外している。同様に、12行目の整合性制約は、ディスクDが同じペグP上のより小さなディスクによってブロックされている場合には、時点TにおいてディスクDを移動することはできないことを表現している。インスタンスで与えられたゴール状況が最大時点Mで達成されなければならないという事実は、13行目の整合性制約で表されます。14行目の最終的な整合性制約は、すべてのディスクDとタイムポイントTに対して、on(D,P,T)が成立するようなペグPが1つだけ存在することを主張しています。この条件は、6行目と7行目のon/3の定義によって、解答の動きに関して暗示されていますが、整合性制約によってそのような知識を明示することで、解答の効率が向上することがわかります。

最後に、16行目の表示部分のメタステートメント（セクション3.1.15で詳述）は、述語move/3の上のアトムだけがプリントされるべきであることを示しており、したがって、インスタンスを記述するために使用される述語や、補助的な述語move/2、on/3、blocked/3を抑制している。
これは、解決策がmove/3以上のアトムによって完全に決定されていることから、解決策をより便利に読むためである。

2.3 Problem Solution

これで「ハノイの塔」のパズルを解く準備が整いました。解答を表すアンサーセットを計算するには、以下のコマンドを実行します。

clingo toh_enc.lp toh_ins.lp

または

gringo toh_enc.lp toh_ins.lp | clasp

ソルバー（ここではclingo）の出力は、以下のようになります。

clingo version 5.5.0
Reading from toh_enc.lp ...
Solving...
Answer: 1
move(4,b,1) move(3,c,2) move(4,c,3) move(2,b,4) move(4,a,5) move(3,b,6) move(4,b,7) move(1,c,8) move(4,c,9) move(3,a,10) move(4,a,11) move(2,c,12) move(4,b,13) move(3,c,14) move(4,c,15)
SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 0.006s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.004s

最初の行は、clingoのバージョンを示しています。続く2行はclingoの状態を示しています。clingoは読み込み中であることをすぐに表示する必要があります。それが終わると、コマンドラインに Solving... と出力します。上の Towers of Hanoi のインスタンスは非常に簡単に解けるので、遅延に気づくことはありませんが、より大きな問題では顕著になります。Answer: で始まる行は，次の行に解集合の(出力)アトムが続くことを示しています．この例では、move/3の真のインスタンスを時点の順に並べているので、そこから次の解を簡単に読み取ることができる：最初の移動はディスク4からペグb、二番目の移動はディスク3からペグc、三番目の移動はディスク4からペグc, 等... ここでは、move/3以上のすべてのアトムが、実際には1つのラインに属していることを示すために「\」を使用している。アトムが印刷される順番には意味がないことに注意してください（答えのセットが見つかる順番にも同じことが言えます）。この解答の下には、問題の満足度が示されており、ソルバーによってSATISFIABLEと報告されています。Modelsで始まる行の1+は、1つの回答セットが見つかったことを示しています。ソルバーへの呼び出しは、マルチショット解法の際に注目されます（セクション4参照）。最後の行では、総実行時間（CPU時間と同様にwall-clock時間）、探索にかかった時間(Solving)、最初の解(1st Model)と不満足度(Unsat)を証明するのにかかった分数などの統計が報告されます。利用可能なオプション、例えば、拡張された統計出力を得るためのオプションについては、セクション7に記載されています。

2.4 Summary

最後に、いくつかの "take-home message "をまとめておきます。ハノイの塔のパズルを解くために、まず、インスタンスを表すファクトを提供しました。述語の選択については議論しませんでしたが、適切なインスタンスの表現は、すでにASPでのモデリングの一部であり、必ずしもここでのように単純ではありません。第二に、任意のインスタンスに適用される問題のエンコーディングを提供した。このエンコーディングは、解の候補を生成し、その本質的な特性を導き出し、解の条件に違反しないことをテストし、最後に出力を特性アトムに投影する部分で構成されています。このエンコーディングがあれば、市販のASPツールを使ってインスタンスを解くことができ、将来発生する可能性のある他のインスタンスに対してもエンコーディングを再利用することができます。

3 Input Languages

このセクションでは、グラウンダーgringo、グラウンダーとソルバーの複合機clingo、ソルバーclaspの入力言語の概要を説明します。セクション3.1では，gringoとclingoの結合入力言語について詳しく説明します．最後に、セクション3.2では、claspが扱う入力について説明する。

3.1 Input Language of gringo and clingo

gringo[47]は、ユーザーが定義した論理プログラム（通常は変数を含む）を、等価な基底プログラム（つまり、変数を含まない）に変換することができるグラウンダーです。gringoの出力はソルバーclasp[39, 44]に接続され、答えのセットを計算します。システムclingoはgringoとclaspを内部的に結合し、基底化と解法の両方を担当します。gringoが基底プログラムを出力するのとは対照的に、clingoは解答セットを返す。

通常、論理プログラムは1つまたは複数の（テキスト）ファイルで指定され、その名前はgringoまたはclingoを呼び出す際の引数として提供されます。以下では、gringoとclingoの入力言語に属する構成要素について説明します。

3.1.1 Terms

すべての(非命題)論理プログラムには、主にアトムの引数を指定するための用語が含まれています(後述)。gringo(およびclingo)の項の文法を図2に示します。

基本的な構成要素は、整数、定数、文字列、変数、およびトークンの_、#sup、#infというシンプルな用語です。整数は、セクション3.1.7で詳しく説明するように、算術式によって表されます。定数と変数は最初の文字で区別され、それぞれ小文字と大文字で表されます。さらに、文字列とは、二重引用符（" ¨"）で囲まれた任意の文字列のことで、\、改行、二重引用符は、それぞれ\、\n、\"でエスケープする必要があります。

定数や文字列がそれ自体を表すのに対し、変数は論理プログラムの言語の中で、変数を持たないすべての用語を表すプレースホルダーです。ルールの中で繰り返される変数名が同じ変数を指すのとは異なり、_というトークンはどこにも現れない無名の変数を表します(_が現れるたびに新しい変数名が作られると考えることもできます)。(これは、_が出現するたびに新しい変数名が作られるように見ることができます)。さらに、すべての無変数項の中で最大と最小の要素を表す特殊な定数#supと#infがあり、その使い方はセクション3.1.12で説明します。

次に、(解釈されない)関数は、(定数のような)名前と1つ以上の引数としてのtermを持つ複合termです。例えば、at(peter,time(12),X)は、定数peter、整数の引数を持つ別の関数time(12)、変数Xの3つの引数を持つ関数です。最後に、タプルがあります。タプルは関数と似ていますが、名前はありません。タプルの例としては、空のタプル()や、4つの要素を持つタプル(at,peter,time(12),X)があります。タプルの末尾には、1要素のタプルを区別するために、コンマ,を付けることができます。例えば、(42,)は1要素のタプルですが、(42)はそうではなく、上記の4つのタプルは(at,peter,time(12),X,)と同等です。

訳注: 「解釈されない関数」Wikipediaより。
解釈されない関数や関数記号とは、その名前とn項形式以外の性質を持たないもので、数理論理学では、定数や変数とともに項を形成するために用いられる。関数記号は、定数や変数とともに項を構成するのに用いられる。

3.1.2 Normal Programs and Integrity Constraints

以下の形式のルールは、通常の論理プログラム(整合性制約あり)で認められます。

\begin{eqnarray*}
\rm{Fact} &:& A_0. \\
\rm{Rule} &:& A_0 &:\!-& \quad L_1, \ldots ,L_n. \\
\rm{Integrity\ Constraint} &:& &:\!-& \quad L_1, \ldots ,L_n.
\end{eqnarray*}

訳注: 以降、Fact:事実、Rule:ルール、Integrity Constraint:整合性制約、と訳す事にします。

ルールや事実の$head\ A$は、定数や関数と同じシンタックス形のアトムである。規則や整合性制約の本文では、$1 \leqslant j \leqslant n$のすべての$L_j$は、A または not A の形式のリテラルで、Aはアトムであり、連接の not はデフォルトの否定を表します。リテラル L がアトムであれば正、そうでなければ負であると言います。ファクトの先頭のアトム$A_0$は無条件に真でなければなりませんが、ルールの直感的な読み方は暗黙に相当します。つまり、ルールのボディにあるすべての正のリテラルが真であり、すべての負のリテラルが満たされていれば、$A_0$は真でなければなりません。一方、整合性制約とは、解決策の候補を制限するルールであり、ルール本体のリテラルが同時に満たされてはならないことを意味します。

すべてのルール、事実、整合性制約を満たす(命題の)アトムの集合を論理プログラムのモデルと呼びます。アトムは、モデルに含まれる場合に限り、真とみなされます。ASPでは、モデル内のすべてのアトムがプログラムからの(非サイクルの)導出を持つ場合、そのモデルを解集合と呼ぶ。論理プログラムの解集合の正式な定義については[51, 48, 64]を参照してください。

そのために、いくつかの小さな例を挙げてみましょう。

a :- b.
b :- a.

aとbが偽のときは、両方のルールの本体も偽なので、ルールは満たされています。さらに、派生する(true)アトムがないことから、空集合が答えの集合であることがわかります。一方、aが真でbが偽の場合は、bodyは成り立つがheadは成り立たないので、第1のルールは不満足です。同様に、bが真でaが真でない場合、第2のルールは満たされません。
両方のルールが満たされているにもかかわらず、aとbは非サイクル的に派生することができません。aはbに依存し、その逆もまた然りです。
つまり、aとbの両方を含む集合は答えの集合ではありません。したがって、空集合が論理プログラムの唯一の解答集合となります。最小化の対象となるaとbを通る正のサイクルが存在すると言います。

次の論理プログラムを考えてみましょう。

a :- not b.
b :- not a.

ここで、空のセットは、両方のルールが満たされていないので、モデルではありません。しかし、aのみ、またはbのみを含む集合はモデルです。
それぞれが答集合であることを確認するために、aはbが偽の場合に規則a :- not b.によって導かれ、同様に、bはaが偽の場合にb :- not a.によって導かれることに注意してください。
なお、aとbの両方を含む集合は、両方が真であると仮定した場合、どちらのアトムも導出できないため、答えの集合ではありません。よって、規則a :- not b.とb :- not a.のbodyは偽です。
したがって、論理プログラムの解答集合には、aとbのどちらかが属することになります。

ファクトと整合性制約の使い方を説明するために、先ほどの論理プログラムを拡張してみましょう。

a :- not b.
b :- not a.
c.
:- c, not b.

c.が事実である以上、アトムcは無条件に真でなければならず、すなわち、すべてのモデルに属することになります。このことから、整合性制約:- c, not b.は、その本体が満たされないようにするためには、bも真でなければならないことを示しています。むしろ、ルールb :- not a.の本体が満たされていることを確認する必要があるので、アトムaは偽でなければなりません。したがって、bとcを含む集合が、この論理プログラムの唯一の答えの集合となります。

上記の例では，命題論理プログラムを用いて，解集合の考え方を説明しました．これは，すべての真のアトムが（非循環的に）導出可能であるような論理プログラムのモデルです．実際には、論理プログラムは命題ではなく、変数を含むschematicルールを含むのが一般的です。次の例はその例です。

Example 3.2.

南極に住む子供がアニメを見ていると、ペンギンではない黄色い鳥が出てきます。子供は、ペンギンは翼が小さいので絶対に飛ばないことを知っていますが、黄色い鳥が飛ぶかどうかはわかりません。この知識は次のようなschematicルールで一般化されます。

    fly(X) :- bird(X), not neg_fly(X).
neg_fly(X) :- bird(X), not     fly(X).
neg_fly(X) :- penguin(X).

第1のルールは、第2のルールに従った逆の場合を除いて、鳥が飛ぶことは一般的に可能であることを表現しています。ペンギンが飛ぶことができないという有限の知識は、第3のルールによって特定されます。

その後、子どもは、黄色い鳥が「tweety」というニワトリで、大好きなペンギンが「tux」と呼ばれていることを知ります。この2つの個体に関する知識は、次のような事実で表されます。

bird(tweety). chicken(tweety).
bird(tux).    penguin(tux).

3つのschematicルールの変数Xをtweetyとtuxでインスタンス化すると、次のようなグランドルールが得られます。

fly(tweety)     :- bird(tweety), not neg_fly(tweety).
fly(tux)        :- bird(tux),    not neg_fly(tux).
neg_fly(tweety) :- bird(tweety), not     fly(tweety).
neg_fly(tux)    :- bird(tux),    not     fly(tux).
neg_fly(tweety) :- penguin(tweety).
neg_fly(tux)    :- penguin(tux).

さらに、tweetyとtuxは鳥であることが知られていること、tuxはペンギンであるがtweetyはペンギンではないこと、ペンギンは絶対に飛ばないことを考慮すると、先ほどの基本ルールを単純化して次のようなルールを得ることができます。

    fly(tweety) :- not neg_fly(tweety).
neg_fly(tweety) :- not     fly(tweety).
neg_fly(tux).

ここで、tweetyは飛んでも飛ばなくてもよいが、tuxは確実に飛ばないことが明らかになりました。このように、上記の3つのschematicルールに対して、tweetyとtuxをインスタンス化した2つの回答セットが存在します。

上記の例では、論理プログラムの言語に関するルールのすべてのインスタンスを表すために、変数がどのように使用されるかを説明しました。実際、グラウンダーのgringo(またはclingoのグラウンディング・コンポーネント)は、等価な命題論理プログラムが得られるように、変数をインスタンス化することに気を配っています。そのために、ルールは安全であることが要求されます。つまり、ルール内のすべての変数は、ルールのボディ内のある正のリテラル(notが先行しないリテラル)に出現しなければなりません。例えば、例3.2の最初の2つのschematicルールは、正のボディにbird(X)を含んでいるので安全です。これはgringo(またはclingo)に、Xに代入される値が鳥に限定されていることを伝えています。

これまでに、term、事実、(通常の)ルール、整合性制約を紹介してきました。このシンプルなコア言語の便利な拡張について説明する前に、ルール（またはファクト）の役割は、ボディが満たされていればヘッドのアトムが真となるように導出できるということを覚えておいてください。これとは異なり、整合性制約はテストを実行しますが、どのアトムも導き出すために使用することはできません。この普遍的な意味は、以下で説明するようなより洗練された言語構造を使用する場合にも適用されます。

3.1.3 Classical Negation

連接not はデフォルトの否定を表しています。つまり、リテラルnot Aは、アトムAが真であると導出されない限り、成立すると仮定されます。これに対して、アトムの古典的な（あるいは強い）否定は、それが派生できる場合にのみ成立します。記号-で示される古典的否定は、アトムの前で許されます。つまり、Aがアトムであれば、-AはAの補数を表すアトムです。Aと-Aの意味的な関係は、単にそれらが同時に成立してはならないということです。したがって、古典的否定は、論理プログラムに明示的に記述することなく、整合性制約:- A, -A.を課すことができる構文上の特徴として理解することができます。
論理プログラムによっては、Aも-Aも解集合に含まれていないことがあり、Aの真偽がともに不明な状態を表しています。

Example 3.3.

古典的な否定を用いると、例3.2のschematicルールを以下のように書き換えることができます。

 fly(X) :- bird(X), not -fly(X).
-fly(X) :- bird(X), not  fly(X).
-fly(X) :- penguin(X).

個体tweetyとtuxが与えられた場合、古典的な否定は、以下の（暗黙の）整合性制約によって表現されます。

:- fly(tweety), -fly(tweety).
:- fly(tux), -fly(tux).

まだ、-fly(tux)とfly(tweety)または-fly(tweety)の2つの解集合があります。
ここで、プログラムに次のような事実を追加するとします。

fly(tux).

すると、fly(tux)は無条件に真でなければならず、-fly(tux)はやはり第3の概略規則のインスタンスによって導かれる。fly(tux)と-fly(tux)の両方を含むすべての解集合候補は、5行目の(暗黙の)整合性制約を引き起こすので、もはや解集合は存在しません。

3.1.4 Disjunction

Disjunctive論理プログラムでは、ルールヘッドのアトム間に接続詞;を使用します。

\begin{eqnarray*}
\rm{Fact} &:& A_0 ; \ldots ; A_m . \\
\rm{Rule} &:& A_0 ; \ldots ; A_m &:\!-& \ L_1, \ldots ,L_n.
\end{eqnarray*}

disjunctiveヘッドは、そのアトムの少なくとも1つが真である場合に成立する。

disjunctive論理プログラムの解集合は、ここでは詳細を述べないが、最小化基準を満たす（接続法ASPの実装方法については[22, 36]を参照）。

単純なdisjunctiveプログラムa;b.は、aを含む解集合とbを含む答集合の2つを持つが、両方のアトムが同時に答集合に属することはないことだけを述べる。

例3.1のルールを追加すると、aとbの両方を含む単一の回答セットが得られます。

これは、ASPにおけるdisjunctionは厳密に排他的でも包括的でもなく、最小化の対象であることを示している。

一般的に、disjunctionの使用は、計算の複雑さを増す可能性があります[21]。そのため、複雑さの理由から選択が必要な場合を除き、接続解除の代わりに「choice constructs」（セクション3.1.12で詳述）を使用することをお勧めします。

3.1.5 Double Negation and Head Literals

gringoの入力言語は、not not Aと書かれる二重のデフォルト否定リテラルもサポートしています。
これらは、正のリテラルが満たされるたびに満たされます。しかし、not A形式の否定リテラルと同様に、二重否定リテラルもnotが先行しているので、プログラムからの（非循環）導出は必要ありません。

Clingoチュートリアル

概要