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

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

Мотивация [ править ]

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

${\ displaystyle p \}$

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

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

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

${\displaystyle p}$	${\displaystyle q}$	${\displaystyle r}$	${\displaystyle s}$
Т	F	F	T .

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

${\displaystyle p\land not{\text{ }}q\rightarrow s.}$

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

${\displaystyle p}$	${\displaystyle q}$	${\displaystyle r}$	${\displaystyle s}$
Т	Т	Т	F .

Таким образом, одна из моделей данной программы является особенной в том смысле, что она правильно отображает поведение разрешения 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}$	${\displaystyle q}$	${\displaystyle r}$	${\displaystyle s}$
Т	F	F	T .

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

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

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

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

понимается как результат замены в этой программе основных условий${\displaystyle 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 }$

Определение [ править ]

Позвольте быть набор правил вида${\displaystyle P}$

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

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

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

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

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

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

Пример [ править ]

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

${\displaystyle p\ }$

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

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

Редукт этой программы относительно IS${\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}}$

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

Минимальность: Любая устойчивая модель логической программы минимальна среди моделей относительно включения множества.${\displaystyle P}$${\displaystyle P}$

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

NP-полнота: имеет ли тестирование конечная земля логика программы стабильной модели является NP-полной .

Отношение к другим теориям отрицания как неудачи [ править ]

Завершение программы [ править ]

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

${\displaystyle p\leftarrow p}$

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

Fangzhen Lin и Yuting Zhao [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}}$

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

Альтернативный подход [Ferraris and Lifschitz, 2005] рассматривает сильное отрицание как часть атома и не требует каких-либо изменений в определении стабильной модели. В этой теории сильного отрицания мы различаем атомы двух видов, положительные и отрицательные , и предполагаем, что каждый отрицательный атом является выражением формы , где - положительный атом. Набор атомов называется когерентным, если он не содержит «дополнительных» пар атомов . Когерентные стабильные модели программы идентичны ее последовательным наборам ответов в смысле [Gelfond and Lifschitz, 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}$

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

Согласно [Gelfond and Lifschitz, 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}}$

(точка с запятой рассматривается как альтернативное обозначение дизъюнкции ). Традиционные правила соответствуют , а ограничения - . Чтобы распространить семантику стабильной модели на дизъюнктивные программы [Gelfond and Lifschitz, 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}$ Σ 2 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\}}$

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

См. Также [ править ]

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

Примечания [ править ]

Ссылки [ править ]

• Н. Бидо и К. Фройдево [1987] Минимализм включает логику по умолчанию и ограниченность . В кн .: Материалы LICS-87, стр. 89–97.
• Т. Эйтер и Г. Готтлоб [1993] Результаты о сложности для дизъюнктивного логического программирования и приложения к немонотонным логикам . В кн .: Материалы ИЛПС-93, стр. 266–278.
• М. ван Эмден и Р. Ковальский [1976] Семантика логики предикатов как языка программирования . Журнал ACM, Vol. 23, страницы 733–742.
• Ф. Фэджес [1994] Согласованность завершения Кларка и существования стабильных моделей . Журнал методов логики в компьютерных науках, Vol. 1, страницы 51–60.
• П. Феррарис [2005] Наборы ответов для теорий высказываний . В кн .: Труды ЛПНМР-05, стр. 119–131.
• П. Феррарис и В. Лифшиц [2005] Математические основы программирования наборов ответов . В: Мы их покажем! Очерки в честь Дов Габбая, Публикации Королевского колледжа, страницы 615–664.
• М. Гельфонд [1987] О стратифицированных аутоэпистемических теориях . В: Proceedings of AAAI-87, pages 207–211.
• М. Гельфонд и В. Лифшиц [1988] Семантика стабильной модели для логического программирования . В: Труды Пятой Международной конференции по логическому программированию (ICLP), страницы 1070–1080.
• М. Гельфонд и В. Лифшиц [1991] Классическое отрицание в логических программах и дизъюнктивных базах данных . Вычислительная техника нового поколения, Vol. 9, страницы 365–385.
• С. Хэнкс и Д. Макдермотт [1987] Немонотонная логика и временная проекция . Искусственный интеллект, Vol. 33, страницы 379–412.
• Ф. Линь и Ю. Чжао [2004] ASSAT: Вычисление наборов ответов логической программы решателями SAT . Искусственный интеллект, Vol. 157, страницы 115–137.
• В. Марек и В.С. Субрахманян [1989] Связь между семантикой логической программы и немонотонными рассуждениями . В: Труды ICLP-89, страницы 600–617.
• Д. Пирс [1997] Новая логическая характеристика стабильных моделей и наборов ответов . В: Немонотонные расширения логического программирования (конспект лекций по искусственному интеллекту 1216), страницы 57–70.
• Р. Рейтер [1980] Логика рассуждений по умолчанию . Искусственный интеллект, Vol. 13, страницы 81–132.