Наименьшая эрбрановская модель

Пусть – логическая программа. Обозначим через множество всех э-моделей программы . Оно не пусто (см. упр. 3). Множество есть э-модель, называемая наименьшей э-моделью.

Предложение 2. .

Пример 10. Эрбрановский базис в примере 1 состоит из 18 атомов (найдите их). При этом в силу предложения 2 наименьшей э-моделью для будет {ОТЕЦ (ИВАН, ПЁТР), ОТЕЦ (ПЁТР, СЕМЁН), ДЕДУШКА (ИВАН, СЕМЁН)} (заметим, что отличными от неё э-моделями являются, например: {ОТЕЦ (ИВАН, СЕМЁН)}, {ОТЕЦ (СЕМЁН, ИВАН), ДЕДУШКА (СЕМЁН, ПЁТР), ДЕДУШКА (ПЁТР, ИВАН)}).

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

Определим отображение из решётки э-интерпретаций в себя. Пусть – э-интерпретация. Тогда { есть основной пример некоторого дизъюнкта из и }

Предложение 3. – э-модель для тогда и только тогда, когда .

Введём обозначения: Ø, , если – непосредственно следующий ординал [3]; если – предельный ординал.

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

Теорема 2[7].

Пример 11. Наименьшая э-модель из примера 10 является, как легко проверить, неподвижной точкой отображения а по теореме 2 и наименьшей его неподвижной точкой.

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

Корректная ответная подстановка для – это такая ответная подстановка что универсальное замыкание формулы есть логическое следствие из

Пример 12. Ответными подстановками в примере 1 могут быть: и др. Не являются ответными, например, подстановки: Корректной ответной подстановкой является лишь подстановка .

Предложение 4. Пусть – ответная подстановка для такая, что формула не содержит переменных. Следующие утверждения эквивалентны друг другу:

а) – корректная ответная подстановка,

б) истинно в любой э-модели для

в) истинно в наименьшей э-модели для

Упражнения:

12. Пусть – непустое множество э-моделей для программы

Доказать, что есть э-модель.

13. Почему – непустое множество?

14. Пусть – конечное множество дизъюнктов, – непустое множество э-моделей для Показать, что не обязательно модель.

15. Проверить, что множество всех э-интерпретаций для программы является полной решёткой относительно теоретико-множественного отношения

16. Пусть – программа вида

Показать, что где , и поэтому .

17. Проверить, что:

а) если цель не содержит переменных (основной дизъюнкт), то единственной возможной ответной подстановкой является

б) предложение 4 в общем случае несправедливо, если не требовать условия отсутствия переменных в