Введение

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

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

Значение отрицания в логических программах тесно связано с двумя теориями немонотонного рассуждения — автоэпистемической логикой и логикой по умолчанию. Открытие этих связей стало ключевым шагом к изобретению семантики стабильных моделей. Синтаксис автоэпистемической логики использует модальный оператор, позволяющий различать истинность и известность. Майкл Гельфонд [1987] предложил интерпретировать в теле правила как "не известно", а правило с отрицанием — как соответствующую формулу автоэпистемической логики. Семантика стабильных моделей в своей базовой форме может рассматриваться как переформулировка этой идеи, избегающая явных ссылок на автоэпистемическую логику. В логике по умолчанию, дефолт (правило по умолчанию) аналогично правилу вывода, но включает, помимо посылок и заключения, список формул, называемых обоснованиями. Дефолт может быть использован для вывода его заключения при условии, что его обоснования согласованы с тем, что известно на данный момент. Николь Бидю и Кристин Фройдво [1987] предложили рассматривать отрицательные атомы в телах правил как обоснования. Например, правило

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

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

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

имеет две стабильные модели, а программа, состоящая из одного правила, не имеет стабильных моделей. Если рассматривать семантику стабильных моделей как описание поведения Prolog в присутствии отрицания, то программы без единственной стабильной модели можно считать неудовлетворительными: они не предоставляют однозначной спецификации для запросов в стиле Prolog. Например, обе вышеуказанные программы не подходят для использования в качестве программ Prolog – разрешение SLDNF не завершается для них. Однако использование стабильных моделей в программировании ответов на основе множеств предоставляет иной взгляд на такие программы. В этой парадигме программирования заданная задача поиска представляется логической программой, так что стабильные модели программы соответствуют решениям. Следовательно, программы с множеством стабильных моделей соответствуют задачам с множеством решений, а программы без стабильных моделей – неразрешимым задачам. Например, задача о восьми ферзях имеет 92 решения; для её решения с помощью программирования ответов на основе множеств мы кодируем её логической программой с 92 стабильными моделями. С этой точки зрения, логические программы с ровно одной стабильной моделью являются довольно специфичными в программировании ответов на основе множеств, подобно многочленам с ровно одним корнем в алгебре.

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

Любая стабильная модель конечной основной программы является не только моделью самой программы, но и моделью ее завершения [Marek and Subrahmanian, 1989]. Однако обратное неверно. Например, завершение программы, состоящей из одного правила, является тавтологией. Модель этой тавтологии является стабильной моделью, но другая ее модель не является стабильной. Франсуа Фаж [1994] обнаружил синтаксическое условие для логических программ, которое исключает подобные контрпримеры и гарантирует стабильность каждой модели завершения программы. Программы, удовлетворяющие этому условию, называются строгими (tight). Фанчжэнь Лин и Ютинг Чжао [2004] показали, как усилить завершение неплотной программы, чтобы все ее нестабильные модели были исключены. Дополнительные формулы, которые они добавляют к завершению, называются формулами циклов.

Хорошо обоснованная семантика

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

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

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

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

Стабильные модели множества предложений

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

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

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