Наименьшая эрбрановская модель
Пусть – логическая программа. Обозначим через
множество всех э-моделей программы
. Оно не пусто (см. упр. 3). Множество
есть э-модель, называемая наименьшей э-моделью.
Предложение 2. .
Пример 10. Эрбрановский базис в примере 1 состоит из 18 атомов (найдите их). При этом в силу предложения 2 наименьшей э-моделью для
будет
{ОТЕЦ (ИВАН, ПЁТР), ОТЕЦ (ПЁТР, СЕМЁН), ДЕДУШКА (ИВАН, СЕМЁН)} (заметим, что отличными от неё э-моделями являются, например:
{ОТЕЦ (ИВАН, СЕМЁН)},
{ОТЕЦ (СЕМЁН, ИВАН), ДЕДУШКА (СЕМЁН, ПЁТР), ДЕДУШКА (ПЁТР, ИВАН)}).
Множество всех подмножеств эрбрановского базиса (т.е. множество всех э-интерпретаций программы
) образует полную решётку [6]относительно частичного порядка, задаваемого теоретико-множественным включением
.
Определим отображение из решётки э-интерпретаций в себя. Пусть
– э-интерпретация. Тогда
{
есть основной пример некоторого дизъюнкта из
и
}
Предложение 3. – э-модель для
тогда и только тогда, когда
.
Введём обозначения: Ø,
, если
– непосредственно следующий ординал [3];
если
– предельный ординал.
Скажем, что интерпретация – наименьшая неподвижная точка отображения
если
– неподвижная точка (т.е.
) и для всех неподвижных точек
отображения
имеем
Наименьшая неподвижная точка отображения
обозначается
. Аналогично определяется наибольшая неподвижная точка:
Теорема 2[7].
Пример 11. Наименьшая э-модель из примера 10 является, как легко проверить, неподвижной точкой отображения
а по теореме 2 и наименьшей его неподвижной точкой.
Пусть – программа,
– цель
Ответной подстановкой для
называется подстановка только для переменных из
но не обязательно для всех. При этом все константы и функции из подстановки считаются уже встретившимися в
.
Корректная ответная подстановка для – это такая ответная подстановка
что универсальное замыкание формулы
есть логическое следствие из
Пример 12. Ответными подстановками в примере 1 могут быть: и др. Не являются ответными, например, подстановки:
Корректной ответной подстановкой является лишь подстановка
.
Предложение 4. Пусть – ответная подстановка для
такая, что формула
не содержит переменных. Следующие утверждения эквивалентны друг другу:
а) – корректная ответная подстановка,
б) истинно в любой э-модели для
в) истинно в наименьшей э-модели для
Упражнения:
12. Пусть – непустое множество э-моделей для программы
Доказать, что есть э-модель.
13. Почему – непустое множество?
14. Пусть – конечное множество дизъюнктов,
– непустое множество э-моделей для
Показать, что
не обязательно модель.
15. Проверить, что множество всех э-интерпретаций для программы является полной решёткой относительно теоретико-множественного отношения
16. Пусть – программа вида
Показать, что где
, и поэтому
.
17. Проверить, что:
а) если цель не содержит переменных (основной дизъюнкт), то единственной возможной ответной подстановкой является
б) предложение 4 в общем случае несправедливо, если не требовать условия отсутствия переменных в