Перегляд вихідного коду сторінки Програмування наборами відповідей

{{Парадигми програмування}}
'''Програмування наборами відповідей''' ({{lang-en|Answer set programming, '''ASP'''}})&nbsp;— це форма [[Декларативне програмування|декларативного програмування]], орієнтованого на складні (насамперед, [[NP-складна задача|NP-складні]]) [[Алгоритм пошуку|задачі пошуку]]. Воно засноване на [[Семантика стійких моделей|стійкій моделі]]&nbsp;семантики&nbsp;[[Логічне програмування|логічного програмування]]. В ASP, задача пошуку зводиться до обчислювання стійкої моделі і ''наборів вирішувачів'' ({{lang-en|answer set solvers}})&nbsp;— програм для генерування стійких моделей, що використовуються для пошуку. Обчислювальний процес, включений в конструкцію набору вирішувачів&nbsp;— є посиленням [[DPLL алгоритм]]у, який завжди є скінченним (на відміну від оцінки запиту в [[Prolog]], що може призвести до [[Нескінченний цикл|нескінченного циклу]]).

Взагалі, ASP включає всі додатки з наборів відповідей для [[представлення знань]]<ref>{{cite book |first=Chitta |last=Baral |title=Knowledge Representation, Reasoning and Declarative Problem Solving |url=https://books.google.com/books?id=iTS4ZdEpGZQC |year=2003 |publisher=Cambridge University Press |isbn=978-0-521-81802-5}}</ref><ref>{{cite book |first=Michael |last=Gelfond |chapter=Answer sets |editor1-first=Frank |editor1-last=van Harmelen |editor2-first=Vladimir |editor2-last=Lifschitz |editor3-first=Bruce |editor3-last=Porter |title=Handbook of Knowledge Representation |url=https://books.google.com/books?id=xwBDylHhJhYC&pg=PA285 |year=2008 |publisher=Elsevier |isbn=978-0-08-055702-1 |pages=285–316 }} [http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/gel07b.pdf as PDF] {{Webarchive|url=https://web.archive.org/web/20160303231241/http://www.depts.ttu.edu/cs/research/krlab/pdfs/papers/gel07b.pdf |date=3 березня 2016 }}</ref> та використання оцінки запитів, типу Prolog для вирішення задач, що виникають у цих додатках.

== Історія ==
[[Автоматизоване планування та диспетчеризація|Планувальний]] метод, запропонований в 1993 році Янісом Дімопулосом, {{Нп|Бернард Небел|Бернардом Небелем||Bernhard Nebel}} і Джонатаном Кехлером<ref>
{{cite book |first1=Y. |last1=Dimopoulos |author2link=Bernhard Nebel |first2=B. |last2=Nebel |first3=J. |last3=Köhler |chapter=Encoding planning problems in non-monotonic logic programs |pages=273–285 |editor1-first=Sam |editor1-last=Steel |editor2-first=Rachid |editor2-last=Alami |title=Recent Advances in AI Planning: 4th European Conference on Planning, ECP'97, Toulouse, France, September 24–26, 1997, Proceedings |url=https://books.google.com/books?id=QSBoQgAACAAJ |year=1997 |publisher=Springer |isbn=978-3-540-63912-1 |volume=1348 |series=Lecture notes in computer science: Lecture notes in artificial intelligence}} [ftp://ftp.informatik.uni-freiburg.de/documents/papers/ki/dimopoulos-etal-ecp97.ps.gz as Postscript]</ref> є раннім прикладом програмування наборами відповідей. Їх підхід заснований на взаємозв'язку проекту зі стійкою моделлю.<ref>
{{cite book |first1=V.S. |last1=Subrahmanian |first2=C. |last2=Zaniolo |chapter=Relating stable models and AI planning domains |editor-first=Leon |editor-last=Sterling |title=Logic Programming: Proceedings of the Twelfth International Conference on Logic Programming |chapterurl=https://books.google.com/books?id=vpGEyZWP1dYC&pg=PA233 |year=1995 |publisher=MIT Press |isbn=978-0-262-69177-2 |pages=233–247}} [http://www.cs.ucla.edu/%7Ezaniolo/papers/iclp95.ps as Postscript]</ref>
Т. Шойнен та І. Німель<ref>{{citation |first1=T. |last1=Soininen |first2=I. |last2=Niemelä  |title=Formalizing configuration knowledge using rules with choices |number=TKO-B142 |institution=Laboratory of Information Processing Science, Helsinki University of Technology |year=1998 |url=http://www.tcs.hut.fi/~ini/papers/sn-faanmr98.ps.gz |format=Postscript}}</ref> 
застосували те, що зараз відомо як ''програмування наборами відповідей'' для розв'язання задачі конфігурації продукту. Використання наборів вирішувачів для пошуку було визначене як нова парадигма програмування {{Нп|Віктор Марек|Віктором Мареком||Victor W. Marek}} і Мар'яном Цужинські в документі, опублікованому в 1999 році.<ref>
{{cite book |first1=V. |last1=Marek |first2=M. |last2=Truszczyński |chapter=Stable models and an alternative logic programming paradigm |editor-first=Krzysztof R. |editor-last=Apt |title=The Logic programming paradigm: a 25-year perspective |url=https://books.google.com/books?id=GIhQAAAAMAAJ |year=1999 |publisher=Springer |isbn=978-3-540-65463-6 |chapterurl=http://xxx.lanl.gov/pdf/cs/9809032 |format=PDF |pages=169–181 |ref={{harvid|Apt|1999}}}}</ref><ref>{{cite journal |first=I. |last=Niemelä |title=Logic programs with stable model semantics as a constraint programming paradigm |journal=Annals of Mathematics and Artificial Intelligence |volume=25 |pages=241–273 |year=1999 |doi=10.1023/A:1018930122475 |url=http://users.ics.aalto.fi/ini/papers/lp-csp-long.ps.gz |format=Postscript,gzipped}}</ref> Дійсно, в новій термінології «набір відповідей», замість «стабільної моделі», був вперше запропонований Ліфшицем<ref>{{cite journal |first=V. |last=Lifschitz |title=Action Languages, Answer Sets, and Planning |year=1999}} In {{harvnb|Apt|1999|pp=357–374}}</ref>, у статті, опублікованій в ретроспективі на роботу Марека-Цужинського.

== Мова програмування наборів відповідей AnsProlog ==
[http://www.tcs.hut.fi/Software/smodels/lparse.ps Lparse]&nbsp;— це назва програми, яка спочатку була створена як інструмент {{Нп|Проблема заземлення символів|заземлення||Symbol grounding problem}} для наборів вирішувачів [http://www.tcs.hut.fi/Software/smodels/ smodels]. Мова, яку приймає Lparse, називається AnsProlog.<ref>{{Cite thesis |type=Ph.D. |title=Superoptimisation: Provably Optimal Code Generation using Answer Set Programming |url=http://opus.bath.ac.uk/20352/1/UnivBath_PhD_2009_T_Crick.pdf |last=Crick |first=Tom |year=2009 |publisher=University of Bath |docket=20352 |accessdate=21 грудня 2016 |archiveurl=https://web.archive.org/web/20160304035502/http://opus.bath.ac.uk/20352/1/UnivBath_PhD_2009_T_Crick.pdf |archivedate=4 березня 2016 |deadurl=yes }}</ref> На сьогодні, вона використовується так само, і в багатьох інших вирішувачах, таких, як [https://web.archive.org/web/20110717180541/http://assat.cs.ust.hk/ assat], [http://www.cs.uni-potsdam.de/clasp/ clasp], [http://www.cs.utexas.edu/users/tag/cmodels/ cmodels], [http://www.tcs.hut.fi/Software/gnt/ gNt], [http://www.cs.uni-potsdam.de/nomore/ nomore++] і [http://www.cs.uky.edu/ai/pbmodels/ pbmodels].

Програма на AnsProlog складається з правил:<syntaxhighlight lang="prolog">
<head> :- <body> .
</syntaxhighlight>Символ <code>:-</code> («if») видаляється, якщо <code><body></code> порожній; такі правила називають ''фактами''. Найпростіший вид правил Lparse є [[Семантика стійких моделей|правила з обмеженнями]].

Ще однією корисною конструкцією цієї мови є ''вибір''. Наприклад, правило<syntaxhighlight lang="prolog">
{p,q,r}.
</syntaxhighlight>каже: вибрати довільно, який з атомів <math>p,q,r</math> включити до стабільної моделі. У lparse-програмі, яка містить це правило вибору і більше ніяких інших правил, є 8 стабільних довільних моделей підмножин <math>\{p,q,r\}</math>. Визначення стабільних моделей було узагальнено до програм з вибором правил.<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> Вибір правил може розглядатися також як абревіатура для пропозиційних формул при [[Семантика стійких моделей|стійкій моделі семантики]].<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 |url=http://arxiv.org/pdf/cs/0312045 |format=PDF}} [http://www.cs.utexas.edu/users/vl/papers/weight.ps as Postscript]</ref>
Наприклад, правило ''вибір'' вище можна розглядати як скорочення для сукупності трьох формул «[[Закон виключеного третього|виключеного третього]]»:
: <math>(p\lor\neg p)\land(q\lor\neg q)\land(r\lor\neg r).</math>
Мова lparse дозволяє нам писати «обмеження» правил вибору, такі як<syntaxhighlight lang="prolog">
1{p,q,r}2.
</syntaxhighlight>
Це правило говорить: вибрати принаймні 1 з атомів, але не більше 2. Сенс цього правила в рамках стійкої моделі семантики є [[Предикат|пропозиційною формулою]]:

<math>(p \lor \thicksim p)\land(q  \lor \thicksim q)\land(r \lor \thicksim r) \land (p \lor q \lor r)\land \thicksim(p \land q\land r)</math>

Границя потужності множини може бути використана в тілі правила, наприклад:<syntaxhighlight lang="prolog">
:- 2{p,q,r}.
</syntaxhighlight>
Додавання цього обмеження в програму Lparse усуває стійкі моделі, які містять щонайменше 2 атоми. Сенс цього правила може бути представлений у вигляді пропозиційної формули

<math>\thicksim((p \land q)\lor(p \land r) \lor(q \land r))</math>.
Змінні (великі літери, як і в [[Пролог (мова програмування)|Пролозі]]), використовуються в Lparse для скорочування колекцій правил, які дотримуються тієї ж схеми, а також для скорочення колекцій атомів в одне і те ж правило. Наприклад, Lparse програма:<syntaxhighlight lang="prolog">
p(a). p(b). p(c).
q(X) :- p(X), X!=a.
</syntaxhighlight>має таке ж значення, як:<syntaxhighlight lang="prolog">
p(a). p(b). p(c).
q(b). q(c).
</syntaxhighlight>Програма:<syntaxhighlight lang="prolog">
p(a). p(b). p(c).
{q(X):-p(X)}2.
</syntaxhighlight>це скорочення:<syntaxhighlight lang="prolog">
p(a). p(b). p(c).
{q(a),q(b),q(c)}2.
</syntaxhighlight>Діапазон має вигляд:<syntaxhighlight lang="prolog">
<Predicate>(start..end)
</syntaxhighlight>
де початок і кінець є константними арифметичними виразами зі значенням. Діапазон&nbsp;— умовне скорочення, яке використовується в основному для визначення числових доменів сумісним способом. Наприклад факт:<syntaxhighlight lang="prolog">
a(1..3).
</syntaxhighlight>Це скорочення:<syntaxhighlight lang="prolog">
a(1). a(2). a(3).
</syntaxhighlight>
Діапазони також можуть бути використані в тілі правила з тією ж семантикою.

''Умовний текст'' має вигляд:<syntaxhighlight lang="prolog">
p(X):q(X)
</syntaxhighlight>
Якщо розширення q є {q(a1); q(a2); … ; q(aN)}, то вищевказана умова семантично еквівалентна запису: p(a1), p(a2), … , p(aN) на місці умови. Наприклад,
<syntaxhighlight lang="prolog">
q(1..2).
a :- 1 {p(X):q(X)}.
</syntaxhighlight>
Це скорочення для
<syntaxhighlight lang="prolog">
q(1). q(2).
a :- 1 {p(1), p(2)}.
</syntaxhighlight>

== Створення стійких моделей ==
Для знаходження стійкої моделі Lparse програми, що зберігається у файлі <code>${filename}</code> використовується команда:<syntaxhighlight lang="console">
% lparse ${filename} | smodels
</syntaxhighlight>Параметр 0 вказує smodels знайти ''всі'' стійкі моделі програми. Наприклад, якщо файл <code>test</code> містить правила:<syntaxhighlight lang="prolog">
1{p,q,r}2.
s :- not p.
</syntaxhighlight>тоді команда видасть:<syntaxhighlight lang="console">
% lparse test | smodels 0
Answer: 1
Stable Model: q p 
Answer: 2
Stable Model: p 
Answer: 3
Stable Model: r p 
Answer: 4
Stable Model: q s 
Answer: 5
Stable Model: r s 
Answer: 6
Stable Model: r q s
</syntaxhighlight>

== Приклади програм ASP ==

=== Фарбування графу ===
''n''-[[Розфарбовування графів|колір]]&nbsp;на [[Граф (математика)|графі]] <math>G = \left\lang V, E\right\rang</math>&nbsp;— це функція <math>color: V\to\{1,\dots,n\}</math> така, що <math>color(x)\neq color(y)</math> для кожної пари суміжних вершин <math>(x,y)\in E</math>. Ми хотіли б використовувати ASP щоб знайти <math>n</math>-кольорів даного графу (або визначити, що його не існує).

Це можна зробити за допомогою наступної програми Lparse:<syntaxhighlight lang="prolog">
c(1..n).                                           
1 {color(X,I) : c(I)} 1 :- v(X).             
:- color(X,I), color(Y,I), e(X,Y), c(I).
</syntaxhighlight>1 рядок визначає номери <math>1,\dots,n</math> кольорів. В залежності від вибору правил у рядку 2, унікальний колір <math>i</math> повиннен бути призначений для кожної вершини <math>x</math>. Обмеження у рядку 3 забороняє призначати один і той же колір до вершини <math>x</math> і <math>y</math> якщо існує ребро, що з'єднує їх.

Якщо поєднати цей файл з визначенням <math>G</math> таким як<syntaxhighlight lang="prolog">
v(1..100). % 1,...,100 are vertices
e(1,55). % there is an edge from 1 to 55
. . .
</syntaxhighlight>і запустити smodels на ньому, з числовим значенням <math>n</math> зазначеним в командному рядку, тоді атоми форми <math>color(\dots,\dots)</math> у вихідних даних smodels будуть представляти собою <math>n</math>-колір <math>G</math>.

Програма в цьому прикладі ілюструє «generate-and-test» організацію, яка часто зустрічається в простих ASP програмах. Правило вибір описує набір «потенційних рішень». Потім слідує обмеження, яке виключає всі можливі рішення, які не прийнятні. Однак, сам процес пошуку, який вживає smodels і інші набори вирішувачів не основані на [[Метод проб і помилок|методі проб і помилок]].

=== Велика кліка ===
[[Кліка (теорія графів)|Клікою]] в графі називають набір попарно суміжних вершин. Наступна lparse-програма знаходить кліку розміру <math>\geq n</math> в даному графі, або визначає, що вона не існує:<syntaxhighlight lang="prolog">
n {in(X) : v(X)}.
:- in(X), in(Y), v(X), v(Y), X!=Y, not e(X,Y), not e(Y,X).
</syntaxhighlight>Це ще один приклад generate-and-test organization. Вибір правил у рядку 1 «створює» всі набори, що складаються з вершин <math>\geq n</math>. Обмеження у рядку 2 «відсіває» ті набори, які не є кліками.

=== Гамільтонів цикл ===
[[Гамільтонів шлях|Гамільтонів цикл]] в [[Орієнтований граф|орієнтованому графі]] є [[Шлях (теорія графів)|цикл]], який проходить через кожну вершину графу рівно один раз. Наступна Lparse програма може бути використана для пошуку Гамільтонівського циклу в заданому орієнтованому графі, якщо він існує; ми припускаємо, що 0&nbsp;— це одна з вершин.
<syntaxhighlight lang="prolog">
{in(X,Y)} :- e(X,Y).

:- 2 {in(X,Y) : e(X,Y)}, v(X).
:- 2 {in(X,Y) : e(X,Y)}, v(Y).

r(X) :- in(0,X), v(X).
r(Y) :- r(X), in(X,Y), e(X,Y).

:- not r(X), v(X).
</syntaxhighlight>
Правило вибору в рядку 1 «створює» всі підмножини набору ребер. Три обмеження «відсіюють» ті підмножини, які не є Гамільтонівськими циклами. Останній з них використовує допоміжний предикат <math>r(x)</math> («<math>x</math> is reachable from 0»), щоб заборонити вершини, які не задовольняють цій умові. Цей предикат визначається рекурсивно в рядках 4 та 5.

Ця програма є прикладом більш загального «generate, define and test» організування, яке включає в себе визначення допоміжного предиката, який допомагає нам усунути все «погане» у потенційному рішенні.

=== Синтаксичний аналіз ===
[[Обробка природної мови]] та [[синтаксичний аналіз]] можуть бути сформульовані як проблема ASP.<ref>{{Cite web |url=http://loqtek.com/?id=course_pars&sec=1 |title=Dependency parsing |accessdate=18 грудня 2016 |archiveurl=https://archive.today/20150415155632/http://loqtek.com/?id=course_pars&sec=1 |archivedate=15 квітня 2015 |deadurl=yes }}</ref>
Наступний код аналізує латинську фразу '''Puella pulchra in villa linguam latinam discit'''&nbsp;— «красива дівчина навчається латині на віллі».
Синтаксичне дерево виражене ''дуговими предикатами'', які позначають залежності між словами в реченні.
Обчислена структура є лінійно впорядкованим кореневим деревом.<syntaxhighlight lang="prolog">
% ********** input sentence **********
word(1, puella). word(2, pulchra). word(3, in). word(4, villa). word(5, linguam). word(6, latinam). word(7, discit).
% ********** lexicon **********
1{ node(X, attr(pulcher, a, fem, nom, sg));
   node(X, attr(pulcher, a, fem, nom, sg)) }1 :- word(X, pulchra).
node(X, attr(latinus, a, fem, acc, sg)) :- word(X, latinam).
1{ node(X, attr(puella, n, fem, nom, sg));
   node(X, attr(puella, n, fem, abl, sg)) }1 :- word(X, puella).
1{ node(X, attr(villa, n, fem, nom, sg));
   node(X, attr(villa, n, fem, abl, sg)) }1 :- word(X, villa).
node(X, attr(linguam, n, fem, acc, sg)) :- word(X, linguam).
node(X, attr(discere, v, pres, 3, sg)) :- word(X, discit).
node(X, attr(in, p)) :- word(X, in).
% ********** syntactic rules **********
0{ arc(X, Y, subj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, nom, sg)).
0{ arc(X, Y, dobj) }1 :- node(X, attr(_, v, _, 3, sg)), node(Y, attr(_, n, _, acc, sg)).
0{ arc(X, Y, attr) }1 :- node(X, attr(_, n, Gender, Case, Number)), node(Y, attr(_, a, Gender, Case, Number)).
0{ arc(X, Y, prep) }1 :- node(X, attr(_, p)), node(Y, attr(_, n, _, abl, _)), X < Y.
0{ arc(X, Y, adv) }1 :- node(X, attr(_, v, _, _, _)), node(Y, attr(_, p)), not leaf(Y).
% ********** guaranteeing the treeness of the graph **********
1{ root(X):node(X, _) }1.
:- arc(X, Z, _), arc(Y, Z, _), X != Y.
:- arc(X, Y, L1), arc(X, Y, L2), L1 != L2.
path(X, Y) :- arc(X, Y, _).
path(X, Z) :- arc(X, Y, _), path(Y, Z).
:- path(X, X).
:- root(X), node(Y, _), X != Y, not path(X, Y).
leaf(X) :- node(X, _), not arc(X, _, _).
</syntaxhighlight>

== Порівняння реалізацій ==
Ранні системи, такі як Smodels, використовували пошук з поверненням, щоб знайти рішення. З розвитком теорії і практики у [[Задача здійсненності бульових формул|задачах здійсненності бульових формул]] (Boolean SAT solvers), збільшувалася кількість ASP вирішувачів, спроектованих на основі SAT-вирішувачів включно з ASSAT та Cmodels. Вони перетворювали ASP формулу в SAT пропозицію, застосували SAT вирішувач, а потім перетворювали рішення назад до ASP форми. Більш сучасні системи, такі як Clasp, використовують гібридний підхід, використовуючи conflict-driven algorithms без повного перетворення в форму булевої логіки. Ці підходи дозволяють значно поліпшити продуктивність, часто на порядок кращі порівняно з попередніми алгоритмами з поверненням.

Проект [http://potassco.sourceforge.net/ Potassco] являє собою «парасольку» для багатьох низькорівневих систем, в тому числі clasp, систему заземлення gringo, та інші.

Більшість систем підтримують змінні, та тільки опосередковано, шляхом примусового заземлення за допомогою заземлюючих систем, таких як ''Lparse'' чи ''gringo''. Необхідність заземлення може призвести до комбінаторних вибухів; таким чином, системи які виконують заземлення на льоту мають перевагу.

{| class="wikitable"
|-
! colspan="3" |Платформа
! colspan="5" | Риси
! colspan="1" |Механіка
|-
! style="background:#ffdead;" |Найменування
! style="background:#ffdead;" |Операційна
система
! style="background:#ffdead;" |Ліцензія
! style="background:#ffdead;" |Змінні
! style="background:#ffdead;" |Функціональні символи
! style="background:#ffdead;" |Явні набори
! style="background:#ffdead;" |Явні списки
! style="background:#ffdead;" |Правила вибору
!
|-
|{{rh}}|[http://www.info.univ-angers.fr/pub/claire/asperix/ ASPeRiX]
|[[Linux]]
|[[GPL]]
|{{yes}}
|
|
|
|{{no}}
|заземлення «на льоту»
|-
|{{rh}}|[https://web.archive.org/web/20110717180541/http://assat.cs.ust.hk/ ASSAT]
|[[Solaris]]
|Безкоштовна
|
|
|
|
|
|заснований на SAT-вирішувачі
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/clasp/ Clasp Answer Set Solver]
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]]
|[[GPL]]
|{{yes}}
|{{yes}}
|{{no}}
|{{no}}
|{{yes}}
|інкрементний, надхненний Sat-вирішувачем
|-
|{{rh}}|[http://www.cs.utexas.edu/users/tag/cmodels/ Cmodels]
|[[Linux]], [[Solaris]]
|[[GPL]]
|Потребує заземлення
|
|
|
|{{yes}}
|інкрементний, надхненний Sat-вирішувачем
|-
|{{rh}}|[[DLV]]
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]]<ref name="dlvsystem.com">{{cite web |url=http://www.dlvsystem.com |title=DLV System company page |publisher=DLVSYSTEM s.r.l. |accessdate=16 листопада 2011}}</ref>
|безкоштовна для академічного та некомерційного використання в освітніх цілях, а також для некомерційних організацій
|{{yes}}
|{{yes}}
|{{no}}
|{{no}}
|{{yes}}
|Не Lparse сумісний
|-
|{{rh}}|[http://www.mat.unical.it/dlv-complex/ DLV-Complex]
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]]
|[[GPL]]
|
|{{yes}}
|{{yes}}
|{{yes}}
|{{yes}}
|побудований на вершині [[DLV]]&nbsp;— не Lparse сумісний
|-
|{{rh}}|[http://www.tcs.hut.fi/Software/gnt/ GnT]
|[[Linux]]
|[[GPL]]
|Потребує заземлення
|
|
|
|{{yes}}
|побудований на вершині smodels
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/nomore/ nomore++]
|[[Linux]]
|[[GPL]]
|
|
|
|
|
|комбінований
|-
|{{rh}}|[http://www.cs.uni-potsdam.de/platypus/ Platypus]
|[[Linux]], [[Solaris]], [[Microsoft Windows|Windows]]
|[[GPL]]
|
|
|
|
|
|розподілений
|-
|{{rh}}|[http://www.cs.uky.edu/ai/pbmodels/ Pbmodels]
|[[Linux]]
|?
|
|
|
|
|
|заснований на псевдобулевському вирішувачі
|-
|{{rh}}|[http://www.tcs.hut.fi/Software/smodels/ Smodels]
|[[Linux]], [[macOS]], [[Microsoft Windows|Windows]]
|[[GPL]]
|Потребує заземлення
|{{no}}
|{{no}}
|{{no}}
|{{no}}
|
|-
|{{rh}}|[http://www.nku.edu/~wardj1/Research/smodels_cc.html Smodels-cc]
|[[Linux]]
|?
|Потребує заземлення
|
|
|
|
|заснований на SAT-вирішувачі
|-
|{{rh}}|[http://www.cs.utexas.edu/users/tag/sup/ Sup]
|[[Linux]]
|?
|
|
|
|
|
|заснований на SAT-вирішувачі
|}

== Див. також ==
* [https://uk.wikipedia.org/w/Логічне%20програмування Логіка програмування]
* [https://uk.wikipedia.org/w/Пролог Пролог]
* [https://uk.wikipedia.org/w/Семантика%20стійких%20моделей Стабільна модель семантики]

== Посилання ==
{{Reflist}}
[[Категорія:Логічне програмування]]
[[Категорія:Статті з прикладами коду мовою Prolog]]