Стабильная модель семантики

Концепция стабильной модели , или набора ответов , используется для определения декларативной семантики для логических программ с отрицанием как неудачей . Это один из нескольких стандартных подходов к значению отрицания в логическом программировании, наряду с завершением программы и обоснованной семантикой . Стабильная семантика модели является основой программирования набора ответов .

Мотивация

Исследование декларативной семантики отрицания в логическом программировании было мотивировано тем фактом, что поведение разрешения SLDNF — обобщения разрешения SLD, используемого Прологом при наличии отрицания в телах правил — не полностью соответствует таблицам истинности, известным из классической пропозициональной логики . Рассмотрим, например, программу

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

При наличии этой программы запрос p будет успешным, потому что программа включает p как факт; запрос q потерпит неудачу, потому что он не встречается в заголовке ни одного из правил. Запрос r также потерпит неудачу, потому что единственное правило с r в заголовке содержит подцель q в своем теле; как мы видели, эта подцель терпит неудачу. Наконец, запрос s будет успешным, потому что каждая из подцелей p , успешна. (Последняя успешна, потому что соответствующая положительная цель q не успешна.) Подводя итог, можно сказать, что поведение разрешения SLDNF в данной программе можно представить следующим назначением истинности: ${\displaystyle \operatorname {not} q}$

С другой стороны, правила данной программы можно рассматривать как пропозициональные формулы, если мы отождествим запятую с союзом , символ с отрицанием и согласимся рассматривать как импликацию, записанную наоборот. Например, последнее правило данной программы является, с этой точки зрения, альтернативной записью для пропозициональной формулы ${\displaystyle \land }$ ${\displaystyle \operatorname {not} }$ ${\displaystyle \neg }$ ${\displaystyle F\leftarrow G}$ ${\displaystyle G\rightarrow F}$

${\displaystyle p\land \neg q\rightarrow s.}$

Если мы вычислим значения истинности правил программы для задания истинности, показанного выше, то мы увидим, что каждое правило получает значение T. Другими словами, это задание является моделью программы. Но эта программа имеет и другие модели, например

Таким образом, одна из моделей данной программы является специальной в том смысле, что она правильно представляет поведение разрешения SLDNF. Каковы математические свойства этой модели, которые делают ее специальной? Ответ на этот вопрос дает определение стабильной модели.

Отношение к немонотонной логике

Значение отрицания в логических программах тесно связано с двумя теориями немонотонных рассуждений — автоэпистемической логикой и логикой по умолчанию . Открытие этих отношений стало ключевым шагом на пути к изобретению стабильной модельной семантики.

Синтаксис автоэпистемической логики использует модальный оператор , который позволяет нам различать то, что истинно, и то, что известно. Майкл Гелфонд [1987] предложил читать текст правила как « неизвестно», а правило с отрицанием понимать как соответствующую формулу автоэпистемической логики. Семантика стабильной модели в ее базовой форме может рассматриваться как переформулировка этой идеи, которая избегает явных ссылок на автоэпистемическую логику. ${\displaystyle \operatorname {not} p}$ ${\displaystyle p}$

В логике по умолчанию, умолчание похоже на правило вывода , за исключением того, что оно включает в себя, помимо своих предпосылок и заключения, список формул, называемых обоснованиями. Умолчание может быть использовано для вывода его заключения при условии, что его обоснования согласуются с тем, что известно в настоящее время. Николь Бидуа и Кристин Фруаво [1987] предложили рассматривать отрицаемые атомы в телах правил как обоснования. Например, правило

${\displaystyle s\leftarrow p,\operatorname {not} q}$

можно понимать как значение по умолчанию, которое позволяет нам выводить из предположения, что является последовательным. Семантика стабильной модели использует ту же идею, но она явно не ссылается на логику по умолчанию. ${\displaystyle s}$ ${\displaystyle p}$ ${\displaystyle \neg q}$

Стабильные модели

Определение стабильной модели ниже, воспроизведенное из [Gelfond and Lifschitz, 1988], использует два соглашения. Во-первых, истинностное назначение идентифицируется с набором атомов, которые получают значение T . Например, истинностное назначение

отождествляется с множеством . Это соглашение позволяет нам использовать отношение включения множества для сравнения истинностных назначений друг с другом. Наименьшее из всех истинностных назначений — это то, которое делает каждый атом ложным; наибольшее истинностное назначение делает каждый атом истинным. ${\displaystyle \{p,s\}}$ ${\displaystyle \emptyset }$

Во-вторых, логическая программа с переменными рассматривается как сокращение для множества всех основных экземпляров ее правил, то есть для результата замены переменных в правилах программы на термины, свободные от переменных, всеми возможными способами. Например, определение четных чисел в логическом программировании

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(X))\leftarrow \operatorname {not} \operatorname {even} (X)}$

понимается как результат замены X в этой программе основными терминами

${\displaystyle 0,s(0),s(s(0)),\dots .}$

всеми возможными способами. Результатом является бесконечная программа заземления

${\displaystyle \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(0))\leftarrow \operatorname {not} \operatorname {even} (0)}$

${\displaystyle \operatorname {even} (s(s(0)))\leftarrow \operatorname {not} \operatorname {even} (s(0))}$

${\displaystyle \dots }$

Определение

Пусть P — набор правил вида

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

где — основные атомы. Если P не содержит отрицания ( в каждом правиле программы), то по определению единственной стабильной моделью P является его модель, минимальная относительно включения множеств. ^[1] (Любая программа без отрицания имеет ровно одну минимальную модель.) Чтобы распространить это определение на случай программ с отрицанием, нам понадобится вспомогательное понятие редукта, определяемое следующим образом. ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$ ${\displaystyle n=0}$

Для любого набора I основных атомов сокращение P относительно I представляет собой набор правил без отрицания, полученный из P путем предварительного отбрасывания каждого правила, такого, что по крайней мере один из атомов ⁠ ⁠ в его теле ${\displaystyle C_{i}}$

${\displaystyle B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

принадлежит I , а затем отбрасывая части из тел всех оставшихся правил. ${\displaystyle \operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

Мы говорим, что I является стабильной моделью P , если I является стабильной моделью редукции P относительно I. (Поскольку редукция не содержит отрицания , ее стабильная модель уже определена.) Как предполагает термин «стабильная модель», каждая стабильная модель P является моделью P.

Пример

Чтобы проиллюстрировать эти определения, давайте проверим, является ли устойчивой модель программы. ${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p,\operatorname {not} q.}$

Сокращение этой программы относительно равно ${\displaystyle \{p,s\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q}$

${\displaystyle s\leftarrow p.}$

(Действительно, поскольку , редукт получается из программы путем отбрасывания части ) Стабильная модель редукта — . (Действительно, этот набор атомов удовлетворяет каждому правилу редукта, и у него нет собственных подмножеств с тем же свойством.) Таким образом, после вычисления стабильной модели редукта мы пришли к тому же набору, с которого начинали. Следовательно, этот набор является стабильной моделью. ${\displaystyle q\not \in \{p,s\}}$ ${\displaystyle \operatorname {not} q.}$ ${\displaystyle \{p,s\}}$ ${\displaystyle \{p,s\}}$

Проверка таким же образом остальных 15 наборов, состоящих из атомов, показывает, что эта программа не имеет других устойчивых моделей. Например, сокращение программы относительно равно ${\displaystyle p,q,r,s}$ ${\displaystyle \{p,q,r\}}$

${\displaystyle p}$

${\displaystyle r\leftarrow p,q.}$

Стабильная модель редукции — это , которая отличается от набора , с которого мы начали. ${\displaystyle \{p\}}$ ${\displaystyle \{p,q,r\}}$

Программы без уникальной стабильной модели

Программа с отрицанием может иметь много устойчивых моделей или не иметь устойчивых моделей. Например, программа

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

имеет две стабильные модели , . Программа с одним правилом ${\displaystyle \{p\}}$ ${\displaystyle \{q\}}$

${\displaystyle p\leftarrow \operatorname {not} p}$

не имеет стабильных моделей.

Если мы думаем о стабильной семантике модели как об описании поведения Пролога в присутствии отрицания, то программы без уникальной стабильной модели можно считать неудовлетворительными: они не предоставляют однозначной спецификации для ответа на запросы в стиле Пролога. Например, две программы выше не являются разумными в качестве программ Пролога — разрешение SLDNF на них не заканчивается.

Но использование стабильных моделей в программировании наборов ответов дает иную перспективу для таких программ. В этой парадигме программирования заданная задача поиска представлена ​​логической программой, так что стабильные модели программы соответствуют решениям. Тогда программы со многими стабильными моделями соответствуют задачам со многими решениями, а программы без стабильных моделей соответствуют неразрешимым задачам. Например, головоломка с восемью королевами имеет 92 решения; чтобы решить ее с помощью программирования наборов ответов, мы кодируем ее логической программой с 92 стабильными моделями. С этой точки зрения логические программы с ровно одной стабильной моделью являются довольно специальными в программировании наборов ответов, как многочлены с ровно одним корнем в алгебре.

Свойства стабильной семантики модели

В этом разделе, как и в определении устойчивой модели выше, под логической программой мы подразумеваем набор правил вида

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

где находятся основные атомы. ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

Головные атомы

Если атом A принадлежит стабильной модели логической программы P , то A является главой одного из правил P.

Минимальность

Любая стабильная модель логической программы P является минимальной среди моделей P относительно включения множеств.

Свойство антицепи

Если I и J являются стабильными моделями одной и той же логической программы, то I не является собственным подмножеством J. Другими словами, множество стабильных моделей программы является антицепью .

NP-полнота

Проверка того, имеет ли конечная логическая программа стабильную модель, является NP-полной .

Отношение к другим теориям отрицания как неудачи

Завершение программы

Любая стабильная модель конечной базовой программы является не только моделью самой программы, но и моделью ее завершения [Marek and Subrahmanian, 1989]. Обратное, однако, неверно. Например, завершение программы с одним правилом

${\displaystyle p\leftarrow p}$

является тавтология . Модель этой тавтологии является стабильной моделью , но другая ее модель — нет. Франсуа Фагес [1994] нашел синтаксическое условие для логических программ, которое устраняет такие контрпримеры и гарантирует стабильность каждой модели завершения программы. Программы, которые удовлетворяют его условию, называются плотными . ${\displaystyle p\leftrightarrow p}$ ${\displaystyle \emptyset }$ ${\displaystyle p\leftarrow p}$ ${\displaystyle \{p\}}$

Фанчжэнь Линь и Ютин Чжао [2004] показали, как сделать завершение нежесткой программы более сильным, так что все ее нестабильные модели будут устранены. Дополнительные формулы, которые они добавляют к завершению, называются формулами цикла .

Обоснованная семантика

Хорошо обоснованная модель логической программы разбивает все основные атомы на три множества: истинные, ложные и неизвестные. Если атом является истинным в хорошо обоснованной модели , то он принадлежит каждой стабильной модели . Обратное, как правило, не выполняется. Например, программа ${\displaystyle P}$ ${\displaystyle P}$

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r\leftarrow p}$

${\displaystyle r\leftarrow q}$

имеет две устойчивые модели, и . Хотя принадлежит обеим из них, его значение в обоснованной модели неизвестно . ${\displaystyle \{p,r\}}$ ${\displaystyle \{q,r\}}$ ${\displaystyle r}$

Более того, если атом ложен в хорошо обоснованной модели программы, то он не принадлежит ни одной из ее стабильных моделей. Таким образом, хорошо обоснованная модель логической программы обеспечивает нижнюю границу пересечения ее стабильных моделей и верхнюю границу их объединения.

Сильное отрицание

Представление неполной информации

С точки зрения представления знаний , набор основных атомов можно рассматривать как описание полного состояния знаний: известно, что атомы, которые принадлежат набору, являются истинными, а атомы, которые не принадлежат набору, являются ложными. Возможно неполное состояние знаний можно описать с помощью последовательного, но, возможно, неполного набора литералов; если атом не принадлежит набору и его отрицание также не принадлежит набору, то неизвестно, является ли он истинным или ложным. ${\displaystyle p}$ ${\displaystyle p}$

В контексте логического программирования эта идея приводит к необходимости различать два вида отрицания — отрицание как неудачу , обсуждавшееся выше, и сильное отрицание , которое здесь обозначается как . ^[2] Следующий пример, иллюстрирующий разницу между двумя видами отрицания, принадлежит Джону Маккарти . Школьный автобус может пересекать железнодорожные пути при условии, что нет приближающегося поезда. Если мы не обязательно знаем, приближается ли поезд, то правило, использующее отрицание как неудачу ${\displaystyle \sim }$

${\displaystyle {\hbox{Cross}}\leftarrow {\hbox{not Train}}}$

не является адекватным представлением этой идеи: оно говорит, что можно переходить дорогу при отсутствии информации о приближающемся поезде. Более слабое правило, которое использует сильное отрицание в теле, предпочтительнее:

${\displaystyle {\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.}$

Там говорится, что переходить дорогу можно, если мы знаем , что поезд не приближается.

Когерентные стабильные модели

Чтобы включить сильное отрицание в теорию устойчивых моделей, Гельфонд и Лифшиц [1991] разрешили каждое из выражений , , в правиле ${\displaystyle A}$ ${\displaystyle B_{i}}$ ${\displaystyle C_{i}}$

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

быть либо атомом, либо атомом с префиксом сильного отрицания. Вместо стабильных моделей это обобщение использует наборы ответов , которые могут включать как атомы, так и атомы с префиксом сильного отрицания.

Альтернативный подход [Феррарис и Лифшиц, 2005] рассматривает сильное отрицание как часть атома, и он не требует никаких изменений в определении стабильной модели. В этой теории сильного отрицания мы различаем атомы двух видов, положительные и отрицательные , и предполагаем, что каждый отрицательный атом является выражением вида , где — положительный атом. Набор атомов называется когерентным, если он не содержит «комплементарных» пар атомов . Когерентные стабильные модели программы идентичны ее согласованным наборам ответов в смысле [Гельфонд и Лифшиц, 1991]. ${\displaystyle {\sim }A}$ ${\displaystyle A}$ ${\displaystyle A,{\sim }A}$

Например, программа

${\displaystyle p\leftarrow \operatorname {not} q}$

${\displaystyle q\leftarrow \operatorname {not} p}$

${\displaystyle r}$

${\displaystyle {\sim }r\leftarrow \operatorname {not} p}$

имеет две устойчивые модели, и . Первая модель является когерентной; вторая — нет, поскольку содержит как атом, так и атом . ${\displaystyle \{p,r\}}$ ${\displaystyle \{q,r,{\sim }r\}}$ ${\displaystyle r}$ ${\displaystyle {\sim }r}$

Предположение о закрытом мире

Согласно [Гельфонду и Лифшицу, 1991], предположение о замкнутости мира для предиката можно выразить правилом ${\displaystyle p}$

${\displaystyle \sim p(X_{1},\dots ,X_{n})\leftarrow \operatorname {not} p(X_{1},\dots ,X_{n})}$

(отношение не выполняется для кортежа, если нет доказательств, что оно выполняется). Например, стабильная модель программы ${\displaystyle p}$ ${\displaystyle X_{1},\dots ,X_{n}}$

${\displaystyle p(a,b)}$

${\displaystyle p(c,d)}$

${\displaystyle \sim p(X,Y)\leftarrow \operatorname {not} p(X,Y)}$

состоит из 2 положительных атомов

${\displaystyle p(a,b),p(c,d)}$

и 14 отрицательных атомов

${\displaystyle \sim p(a,a),{\sim }p(a,c),\dots }$

т.е. сильные отрицания всех других положительных основных атомов, образованных из . ${\displaystyle p,a,b,c,d}$

Логическая программа с сильным отрицанием может включать правила предположения замкнутого мира для некоторых своих предикатов и оставлять другие предикаты в области предположения открытого мира .

Программы с ограничениями

Семантика стабильной модели была обобщена на многие виды логических программ, отличные от наборов «традиционных» правил, обсуждавшихся выше — правил вида

${\displaystyle A\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

где атомы. Одно простое расширение позволяет программам содержать ограничения — правила с пустой головой: ${\displaystyle A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}}$

${\displaystyle \leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}.}$

Напомним, что традиционное правило можно рассматривать как альтернативную запись для пропозициональной формулы, если мы отождествляем запятую с союзом , символ с отрицанием и соглашаемся рассматривать как импликацию, записанную наоборот. Чтобы распространить это соглашение на ограничения, мы отождествляем ограничение с отрицанием формулы, соответствующей ее телу: ${\displaystyle \land }$ ${\displaystyle \operatorname {not} }$ ${\displaystyle \neg }$ ${\displaystyle F\leftarrow G}$ ${\displaystyle G\rightarrow F}$

${\displaystyle \neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).}$

Теперь мы можем расширить определение стабильной модели на программы с ограничениями. Как и в случае с традиционными программами, для определения стабильных моделей мы начинаем с программ, не содержащих отрицания. Такая программа может быть несогласованной; тогда мы говорим, что у нее нет стабильных моделей. Если такая программа непротиворечива, то у нее есть уникальная минимальная модель, и эта модель считается единственной стабильной моделью . ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$

Далее, стабильные модели произвольных программ с ограничениями определяются с помощью редуктов, сформированных так же, как и в случае традиционных программ (см. определение стабильной модели выше). Набор атомов является стабильной моделью программы с ограничениями, если редукт относительно имеет стабильную модель, и эта стабильная модель равна . ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle I}$

Свойства стабильной семантики модели, изложенные выше для традиционных программ, сохраняются и при наличии ограничений.

Ограничения играют важную роль в программировании набора ответов , поскольку добавление ограничения в логическую программу влияет на набор стабильных моделей очень простым способом: оно устраняет стабильные модели, которые нарушают ограничение. Другими словами, для любой программы с ограничениями и любым ограничением стабильные модели можно охарактеризовать как стабильные модели, которые удовлетворяют . ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle C}$ ${\displaystyle P\cup \{C\}}$ ${\displaystyle P}$ ${\displaystyle C}$

Дизъюнктивные программы

В дизъюнктивном правиле голова может быть дизъюнкцией нескольких атомов:

${\displaystyle A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},\operatorname {not} C_{1},\dots ,\operatorname {not} C_{n}}$

(точка с запятой рассматривается как альтернативная нотация для дизъюнкции ). Традиционные правила соответствуют , а ограничения — . Чтобы расширить семантику стабильной модели на дизъюнктивные программы [Гельфонд и Лифшиц, 1991], мы сначала определяем, что при отсутствии отрицания ( в каждом правиле) стабильные модели программы являются ее минимальными моделями. Определение редукции для дизъюнктивных программ остается таким же, как и прежде. Набор атомов является стабильной моделью , если является стабильной моделью редукции относительно . ${\displaystyle \lor }$ ${\displaystyle k=1}$ ${\displaystyle k=0}$ ${\displaystyle n=0}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$

Например, множество является устойчивой моделью дизъюнктивной программы ${\displaystyle \{p,r\}}$

${\displaystyle p;q}$

${\displaystyle r\leftarrow \operatorname {not} q}$

потому что это одна из двух минимальных моделей редукции

${\displaystyle p;q}$

${\displaystyle r.}$

В приведенной выше программе есть еще одна стабильная модель: . ${\displaystyle \{q\}}$

Как и в случае традиционных программ, каждый элемент любой стабильной модели дизъюнктивной программы является головным атомом , в том смысле, что он встречается в голове одного из правил . Как и в традиционном случае, стабильные модели дизъюнктивной программы минимальны и образуют антицепь. Проверка того, имеет ли конечная дизъюнктивная программа стабильную модель, является -полной [Eiter and Gottlob, 1993]. ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle \Sigma _{2}^{\rm {P}}}$

Стабильные модели множества пропозициональных формул

Правила, и даже дизъюнктивные правила, имеют довольно специальную синтаксическую форму по сравнению с произвольными пропозициональными формулами . Каждое дизъюнктивное правило по сути является импликацией, такой что его антецедент (тело правила) является конъюнкцией литералов , а его консеквент (голова) является дизъюнкцией атомов. Дэвид Пирс [1997] и Паоло Феррарис [2005] показали, как расширить определение стабильной модели на наборы произвольных пропозициональных формул. Это обобщение имеет приложения для ответа на программирование множеств .

Формулировка Пирса выглядит совсем не так, как изначальное определение стабильной модели. Вместо редуктов она ссылается на равновесную логику — систему немонотонной логики , основанную на моделях Крипке . Формулировка Феррариса, с другой стороны, основана на редуктах, хотя процесс построения редукта, который она использует, отличается от описанного выше. Два подхода к определению стабильных моделей для наборов пропозициональных формул эквивалентны друг другу.

Общее определение стабильной модели

Согласно [Ferraris, 2005], редукция пропозициональной формулы относительно набора атомов — это формула, полученная из заменой каждой максимальной подформулы, которая не удовлетворяется с помощью логической константы (ложь). Редукция набора пропозициональных формул относительно состоит из редукций всех формул из относительно . Как и в случае дизъюнктных программ, мы говорим, что набор атомов является устойчивой моделью , если является минимальным (относительно включения множеств) среди моделей редукции относительно . ${\displaystyle F}$ ${\displaystyle I}$ ${\displaystyle F}$ ${\displaystyle I}$ ${\displaystyle \bot }$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$ ${\displaystyle P}$ ${\displaystyle I}$

Например, сокращение множества

${\displaystyle \{p,p\land q\rightarrow r,p\land \neg q\rightarrow s\}}$

относительно есть ${\displaystyle \{p,s\}}$

${\displaystyle \{p,\bot \rightarrow \bot ,p\land \neg \bot \rightarrow s\}.}$

Так как является моделью редукта, а собственные подмножества этого множества не являются моделями редукта, то является устойчивой моделью данного набора формул. ${\displaystyle \{p,s\}}$ ${\displaystyle \{p,s\}}$

Мы видели, что также является стабильной моделью той же формулы, записанной в нотации логического программирования, в смысле исходного определения. Это пример общего факта: в применении к набору (формул, соответствующих) традиционных правил определение стабильной модели по Феррарису эквивалентно исходному определению. То же самое верно, в более общем смысле, для программ с ограничениями и для дизъюнктивных программ. ${\displaystyle \{p,s\}}$

Свойства общей стабильной семантики модели

Теорема, утверждающая, что все элементы любой стабильной модели программы являются головными атомами, может быть распространена на наборы пропозициональных формул, если мы определим головные атомы следующим образом. Атом является головным атомом набора пропозициональных формул, если хотя бы одно вхождение в формуле из не находится ни в области отрицания, ни в антецеденте импликации. (Мы предполагаем здесь, что эквивалентность рассматривается как сокращение, а не примитивная связка.) ${\displaystyle P}$ ${\displaystyle P}$ ${\displaystyle A}$ ${\displaystyle P}$ ${\displaystyle A}$ ${\displaystyle P}$

Минимальность и свойство антицепи стабильных моделей традиционной программы не выполняются в общем случае. Например, (синглтон-множество, состоящее из) формулы

${\displaystyle p\lor \neg p}$

имеет две стабильные модели, и . Последняя не является минимальной, и является надлежащим надмножеством первой. ${\displaystyle \emptyset }$ ${\displaystyle \{p\}}$

Проверка того, имеет ли конечный набор пропозициональных формул стабильную модель, является -полной , как и в случае дизъюнктных программ. ${\displaystyle \Sigma _{2}^{\rm {P}}}$

Смотрите также

• Программирование набора ответов
• Логическое программирование
• Отрицание как неудача

Примечания

1. Этот подход к семантике логических программ без отрицания принадлежит Маартену ван Эмдену и Роберту Ковальски — van Emden & Kowalski 1976.
2. Гельфонд и Лифшиц (1991) называют второе отрицание классическим и обозначают его как . ${\displaystyle \neg }$

Ссылки

• Bidoit, N.; Froidevaux, C. (1987). "Minimalism subsums default logic and circumscription". Труды: Symposium on Logic in Computer Science , Итака, Нью-Йорк, 22-25 июня 1987 г. IEEE Computer Society Press. стр. 89–97. ISBN 978-0-8186-0793-6. 87CH2464-6.
• Эйтер, Т.; Готтлоб, Г. (1993). «Результаты сложности для дизъюнктивного логического программирования и применение к немонотонным логикам». ILPS '93: Труды международного симпозиума 1993 года по логическому программированию . MIT Press. стр. 266–278. ISBN 978-0-262-63152-5.
• ван Эмден, М.; Ковальски, Р. (1976). "Семантика предикатной логики как языка программирования" (PDF) . Журнал ACM . 23 (4): 733–742. CiteSeerX  10.1.1.64.9246 . doi :10.1145/321978.321991. S2CID  11048276.
• Фагес, Ф. (1994). «Последовательность завершения Кларка и существование стабильных моделей». Журнал методов логики в информатике . 1 : 51–60. CiteSeerX  10.1.1.48.2157 .
• Феррарис, П. (2005). «Наборы ответов для пропозициональных теорий». Логическое программирование и немонотонные рассуждения. LPNMR 2005. Конспект лекций по информатике. Том 3662. Springer. С. 119–131. CiteSeerX  10.1.1.129.5332 . doi :10.1007/11546207_10. ISBN 978-3-540-31827-9.
• Феррарис, П.; Лифшиц, В. (2005). «Математические основы программирования наборов ответов». Мы им покажем! Эссе в честь Дова Габбея . Издательство King's College Publications. стр. 615–664. CiteSeerX  10.1.1.79.7622 .
• Гельфонд, М. (1987). «О стратифицированных автоэпистемических теориях» (PDF) . AAAI'87: Труды шестой Национальной конференции по искусственному интеллекту . стр. 207–211. ISBN 978-0-934613-42-2.
• Гельфонд, М.; Лифшиц, В. (1988). "Семантика стабильной модели для логического программирования". Труды Пятой международной конференции по логическому программированию (ICLP) . MIT Press. С. 1070–80. ISBN 978-0-262-61054-4.
• Гельфонд, М.; Лифшиц, В. (1991). «Классическое отрицание в логических программах и дизъюнктивных базах данных». New Generation Computing . 9 (3–4): 365–385. CiteSeerX  10.1.1.49.9332 . doi :10.1007/BF03037169. S2CID  13036056.
• Хэнкс, С.; Макдермотт, Д. (1987). «Немонотонная логика и временная проекция». Искусственный интеллект . 33 (3): 379–412. doi :10.1016/0004-3702(87)90043-9.
• Линь, Ф.; Чжао, И. (2004). "ASSAT: Вычисление наборов ответов логической программы с помощью решателей SAT" (PDF) . Искусственный интеллект . 157 (1–2): 115–137. doi :10.1016/j.artint.2004.04.004. S2CID  514581.
• Марек, В.; Субрахманян, В.С. (1989). «Связь между семантикой логической программы и немонотонным рассуждением». Логическое программирование: Труды Шестой международной конференции . MIT Press. С. 600–617. ISBN 978-0-262-62065-9.
• Пирс, Д. (1997). "Новая логическая характеристика стабильных моделей и наборов ответов" (PDF) . Немонотонные расширения логического программирования . Конспект лекций по искусственному интеллекту. Том 1216. С. 57–70. doi :10.1007/BFb0023801. ISBN 978-3-540-68702-3.
• Рейтер, Р. (1980). «Логика для рассуждений по умолчанию» (PDF) . Искусственный интеллект . 13 (1–2): 81–132. doi :10.1016/0004-3702(80)90014-4.