Поняття стійко́ї моде́лі (), або набору відповідей, застосовується для визначення декларативних семантик для логічних програм із запереченням як відмовою. Це один із декількох стандартних підходів до значення заперечення в логічному програмуванні, поряд із повнотою програми та . Семантики стійких моделей є основою програмування наборами відповідей.

Обґрунтування

Дослідження декларативних семантик заперечення в логічному програмуванні спонукав той факт, що поведінка ВЛВЗВ-резолюції, — узагальнення ВЛВ-резолюції, застосовуваного Прологом, — за наявності заперечень у тілах правил не повністю відповідає таблицям істинності, знайомим із класичної логіки висловлень. Розгляньмо, наприклад, програму

За цієї програми запит досягне успіху, оскільки програма включає як факт; запит зазнає невдачі, оскільки він не зустрічається в голові жодного з правил. Запит також зазнає невдачі, оскільки єдине правило з у голові містить підціль у своєму тілі; як ми вже бачили, ця підціль зазнає невдачі. Нарешті, запит досягає успіху, оскільки досягає успіху кожна з його підцілей та . (Остання досягає успіху, оскільки відповідна ствердна ціль зазнає невдачі.) У підсумку, поведінку ВЛВЗВ-резолюції даної програми може бути представлено таким приписуванням істинності:

TFFT.

З іншого боку, правила даної програми можуть розглядатися як предикати, якщо ми ідентифікуємо кому з кон'юнкцією , символ  — із запереченням , і погодимося розглядати як імплікацію , записану навпаки. Наприклад, крайнє правило програми з цієї точки зору є альтернативним записом предикату

Якщо ми обчислимо значення істинності правил програми для наведених вище приписувань істинності, то ми побачимо, що кожне правило набуває значення T. Іншими словами, що приписування є моделлю програми. Але ця програма має також й інші моделі, наприклад,

TTTF.

Таким чином, одна з моделей даної програми є особливою в тому сенсі, що вона правильно представляє поведінку ВЛВЗВ-резолюції. Якими є математичні властивості такої моделі, що роблять її особливою? Відповідь на це питання дає визначення стійкої моделі.

Зв'язок із немонотонною логікою

Значення заперечення в логічних програмах тісно пов'язане з двома теоріями немонотонного міркування — та . Відкриття цих зв'язків стало ключовим кроком до винаходження семантик стійких моделей.

Синтаксис автоепістемної логіки використовує , який дозволяє розрізняти, що є істинним, а чому вірять. 1987 року запропонувавM. Gelfond On stratified autoepistemic theories . In: Proceedings of AAAI-87, pages 207—211. читати в тілі правила як « немає віри», і розуміти правило із запереченням як відповідну формулу автоепістемної логіки. Семантика стійких моделей в її найпростішому вигляді може розглядатися як переформулювання цієї ідеї, що уникає явних посилань на автоепістемну логіку.

В логіці замовчувань замовчування подібне до правила висновування, за виключенням того, що воно, крім своїх передумов та висновку, включає перелік формул, що називаються підтвердженнями (). Замовчування може використовуватися для виведення його висновків за припущення, що його підтвердження узгоджуються з поточними переконаннями. Ніколь Бідуа та Крістін Фруадво 1987 року запропонувалиN. Bidoit and C. Froidevaux Minimalism subsumes default logic and circumscription. In: Proceedings of LICS-87, pages 89–97. розглядати заперечні атоми в тілах правил як підтвердження. Наприклад, правило

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

Стійкі моделі

Наведене нижче визначення стійкої моделіM. Gelfond and V. Lifschitz The stable model semantics for logic programming. In: Proceedings of the Fifth International Conference on Logic Programming (ICLP), pages 1070—1080. використовує дві умови. По-перше, приписування істинності ототожнюється з набором атомів, що набувають значення T. Наприклад, приписування істинності

TFFT.

ототожнюється із набором . Ця умова дозволяє використовувати відношення входження до цього набору для порівняння приписувань істинності між собою. Найменше з усіх приписувань істинності, , є таким, яке робить кожен атом хибним; найбільше приписування істинності робить кожен атом істинним.

По-друге, логічна програма зі змінними розглядається як скорочений запис набору всіх замкнених примірників її правил, тобто результату підставлення вільних від змінних термів замість змінних до правил цієї програми всіма можливими способами. Наприклад, визначення парних () чисел засобами логічного програмування

розглядається як результат заміни у цій програмі замкненими термами

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

Визначення

Нехай буде набором правил вигляду

де є замкненими атомами. Якщо не містить заперечення ( у кожному з правил програми), тоді, за визначенням, єдиною стійкою моделлю є його модель, яка є мінімальною відносно включення правил.M. van Emden and R. Kowalski The semantics of predicate logic as a programming language. Journal of ACM, Vol. 23, pages 733—742. (Будь-яка програма без заперечення має рівно одну мінімальну модель.) Для розширення цього визначення на випадок програм із запереченням нам потрібне додаткове поняття збіднення (), визначене наступним чином.

Для будь-якого набору замкнених атомів збідненням () відносно є набір правил без заперечення, отриманий з спершу виключенням кожного такого правила, в якому щонайменше один із атомів в його тілі

належить до , а потім виключенням частин з тіл усіх правил, що лишилися.

Кажуть, що є стійкою моделлю , якщо є стійкою моделлю збіднення відносно . (Оскільки збіднення не містить заперечення, його стійку модель вже було визначено.) Як підказує термін «стійка модель», кожна стійка модель є моделлю .

Приклад

Щоби проілюструвати ці визначення, перевірмо, чи є стійкою моделлю програми

Збідненням цієї програми відносно є

(Справді, оскільки , збіднення отримується з програми виключенням частини ) Стійкою моделлю збіднення є . (Справді, цей набір атомів задовольняє кожне правило збіднення, і не має власного включення із такою ж властивістю.) Таким чином, після обчислення стійкої моделі збіднення ми повернулися до того ж самого набору , з якого й починали. Отже, цей набір і є стійкою моделлю.

Перевірка таким самим чином інших 15 наборів з атомів показує, що ця програма не має інших стійких моделей. Наприклад, збідненням програми відносно є

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

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

Програма з запереченням може мати багато стійких моделей, та не мати їх взагалі. Наприклад, програма

має дві стійкі моделі, та . Програма з одного правила

не має стійких моделей.

Якщо ми думаємо про семантику стійких моделей як про опис поведінки Прологу в присутності заперечення, то програми без унікальної стійкої моделі можуть розцінюватися як незадовільні: вони не забезпечують недвозначного визначення для надавання відповідей на запити в стилі Прологу. Наприклад, наведені вище дві програми як Прологові програми є нерозумними — ВЛВЗВ-резолюція на них не добігає кінця.

Але застосування стійких моделей в програмуванні наборами відповідей пропонує таким програмам іншу перспективу. В цій парадигмі програмування дана задача пошуку представляється такою логічною програмою, стійкі моделі якої відповідають розв'язкам. Тоді програми з багатьма стійкими моделями відповідають задачам з багатьма розв'язками, а програми без стійких моделей відповідають нерозв'язним задачам. Наприклад, задача про вісім ферзів має 92 розв'язки; щоби розв'язати її із застосуванням програмування наборами відповідей, ми кодуємо її логічною програмою з 92 стійкими моделями. З цієї точки зору логічні програми з рівно однією стійкою моделлю в програмуванні наборами відповідей є радше особливими, як многочлени з рівно одним коренем в алгебрі.

Властивості семантики стійких моделей

В цьому розділі, як і в визначенні стійкої моделі вище, під логічною програмою ми розуміємо набір правил вигляду

де є замкненими атомами.

Атоми голів (): Якщо атом належить до стійкої моделі логічної програми , то є головою одного з правил .

Мінімальність (): Будь-яка стійка модель логічної програми є мінімальною серед моделей відносно включення до набору.

Антиланцюгова властивість (): Якщо та є стійкими моделями однієї й тієї ж логічної програми, то не є власним включенням . Іншими словами, набір стійких моделей програми є антиланцюгом.

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

Зв'язок з іншими теоріями заперечення як відмови

Повнота програми

Будь-яка стійка модель скінченної замкненої програми є моделлю не лише самої програми, а й її повної програми.V. Marek and V.S. Subrahmanian The relationship between logic program semantics and non-monotonic reasoning. In: Proceedings of ICLP-89, pages 600—617. Обернене твердження, проте, не є вірним. Наприклад, повною програмою для програми з одного правила

є тавтологія . Модель цієї тавтології є стійкою моделлю , але інша її модель, , — ні. Франсуа Фаж 1994 року знайшовF. Fages Consistency of Clark's completion and existence of stable models. Journal of Methods of Logic in Computer Science, Vol. 1, pages 51–60. синтаксичну умову для логічних програм, що усуває такі контрприклади, і гарантує стійкість кожної моделі повноти програми. Програми, які задовольняють цю умову, називаються цупкими ().

Фанжен Лін та Ютін Жао 2004 року показали,F. Lin and Y. Zhao ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence, Vol. 157, pages 115—137. як робити повну програму нецупкої програми сильнішою, так що всі її нестійкі моделі буде усунено. Додаткові формули, які вони додають до повної програми, називаються цикловими формулами ().

Добре обґрунтована семантика

логічної програми поділяє всі замкнені атоми на три набори: істинні, хибні та невідомі. Якщо атом є істинним у добре обґрунтованій моделі програми , то він належить до кожної стійкої моделі . Зворотне, взагалі кажучи, не має місця. Наприклад, програма

має дві стійкі моделі, та . Навіть незважаючи на те, що належить до них обох, його значенням у добре обґрунтованій моделі є невідоме.

Крім того, якщо атом є хибним у добре обґрунтованій моделі програми, то він не належить до жодної з її стійких моделей. Таким чином, добре обґрунтована модель логічної програми пропонує нижню межу перетину її стійких моделей, та верхню межу їхнього об'єднання.

Сильне заперечення

Представлення неповної інформації

З точки зору представлення знань набір замкнених атомів може розглядатися як опис повного стану знань: про атоми, що належать до набору, відомо, що вони істинні, а про атоми, що не належать до набору, відомо, що вони хибні. Можливо неповний стан знання може бути описано із застосуванням несуперечливого, але можливо неповного набору літералів; якщо атом не належить до цього набору, і його заперечення також не належить до цього набору, то не відомо, чи є істинним.

В контексті логічного програмування ця ідея призводить до потреби розрізнювати два типи заперечення — заперечення як відмови, обговорюваного вище, та сильного заперечення (), що позначається тут через .Гельфонд та Ліфшиць у праці 1991 року називають друге заперечення класичним (), і позначають його через .M. Gelfond and V. Lifschitz Classical negation in logic programs and disjunctive databases. New Generation Computing, Vol. 9, pages 365—385. Наступний приклад, який показує різницю між цими двома типами заперечення, належить Джонові Маккарті. Шкільний автобус може перетнути () залізничну колію за умови, що не наближається потяг (). Якщо ми не обов'язково знаємо, чи наближається потяг, то правило з використанням заперечення як відмови