Семантика стабильной модели - Stable model semantics - Wikipedia

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

Мотивация

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

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

ТFFТ.

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

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

ТТТF.

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

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

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

Синтаксис аутоэпистемической логики использует модальный оператор это позволяет нам отличать истину от того, во что верят. Майкл Гельфонд [1987] предложил читать в теле правила как " не верится ", и понимать правило с отрицанием как соответствующую формулу аутоэпистемической логики. Семантику стабильной модели в ее базовой форме можно рассматривать как переформулировку этой идеи, которая избегает явных ссылок на аутоэпистемическую логику.

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

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

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

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

ТFFТ.

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

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

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

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

Определение

Позволять быть набором правил формы

куда являются основными атомами. Если не содержит отрицания ( в каждом правиле программы), то по определению единственная устойчивая модель является его моделью, минимальной относительно включения множества.[1] (Любая программа без отрицания имеет ровно одну минимальную модель.) Чтобы распространить это определение на случай программ с отрицанием, нам понадобится вспомогательная концепция редукции, определяемая следующим образом.

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

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

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

Пример

Чтобы проиллюстрировать эти определения, проверим, что стабильная модель программы

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

(Действительно, поскольку , редукт получается из программы отбрасыванием части ) Устойчивая модель редукта . (Действительно, этот набор атомов удовлетворяет каждому правилу редукта, и у него нет собственных подмножеств с таким же свойством.) Таким образом, после вычисления стабильной модели редукта мы пришли к тому же самому набору с чего мы начали. Следовательно, этот набор является стабильной моделью.

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

Стабильная модель редукта , который отличается от множества с чего мы начали.

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

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

имеет две стабильные модели , . Программа одного правила

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

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

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

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

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

куда являются основными атомами.

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

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

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

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

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

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

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

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

Fangzhen Lin и Yuting Zhao [2004] показали, как сделать завершение нестабильной программы более сильным, чтобы все ее нестабильные модели были исключены. Дополнительные формулы, которые они добавляют к завершению, называются формулы цикла.

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

В обоснованная модель логической программы разбивает все основные атомы на три набора: истинное, ложное и неизвестное. Если атом верен в хорошо обоснованной модели то он принадлежит каждой стабильной модели . Обратное, как правило, неверно. Например, программа

имеет две стабильные модели, и . Хотя принадлежит им обоим, его ценность в обоснованной модели составляет неизвестный.

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

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

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

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

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

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

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

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

Чтобы включить сильное отрицание в теорию стабильных моделей, Гельфонд и Лифшиц [1991] разрешили каждое из выражений , , в правиле

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

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

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

имеет две стабильные модели, и . Первая модель последовательна; второй нет, потому что он содержит как атом и атом .

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

Согласно [Gelfond, Lifschitz, 1991], предположение о закрытом мире для предиката можно выразить правилом

(Соотношение не выполняется для кортежа если нет доказательств того, что это так). Например, стабильная модель программы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(точка с запятой рассматривается как альтернативное обозначение дизъюнкции ). Традиционные правила соответствуют , и ограничения к . Чтобы расширить семантику стабильной модели на дизъюнктивные программы [Gelfond and Lifschitz, 1991], мы сначала определяем, что при отсутствии отрицания ( в каждом правиле) стабильными моделями программы являются ее минимальные модели. Определение редукции для дизъюнктивных программ остается так же, как прежде. Множество атомов - это стабильная модель из если стабильная модель редукции относительно .

Например, набор стабильная модель дизъюнктивной программы

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

В приведенной выше программе есть еще одна стабильная модель, .

Как и в случае с традиционными программами, каждый элемент любой стабильной модели дизъюнктивной программы это головной атом , в том смысле, что это происходит в заголовке одного из правил . Как и в традиционном случае, устойчивые модели дизъюнктивной программы минимальны и образуют антицепь. Проверка наличия стабильной модели у конечной дизъюнктивной программы -полный [Эйтер и Готтлоб, 1993].

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

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

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

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

Согласно [Ferraris, 2005], сокращать пропозициональной формулы относительно набора атомов - формула, полученная из заменяя каждую максимальную подформулу, которая не удовлетворяется с логической константой (ложный). В сокращать набора пропозициональных формул относительно состоит из редуктов всех формул из относительно . Как и в случае дизъюнктивных программ, мы говорим, что множество атомов - это стабильная модель из если является минимальным (по включению множества) среди моделей редукции относительно .

Например, редукция множества

относительно является

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

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

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

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

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

имеет две стабильные модели, и . Последний не является минимальным, и он является надстройкой первого.

Проверка того, имеет ли конечный набор пропозициональных формул стабильную модель: -полный, как и в случае дизъюнктивные программы.

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

Примечания

  1. ^ Такой подход к семантике логических программ без отрицания принадлежит Маартену ван Эмдену и Роберт Ковальски [1976].
  2. ^ Гельфонд и Лифшиц [1991] называют второе отрицание классический и обозначим его .

Рекомендации