Законы взаимовырадимости

Д.З: Для каждой великой вещи найдется вещь величиной еще больше и для каждой вещи малой найдется вещь в которую частица меньшая.

Преобразование предикатных формул и их приведение к нормальной, сколемовской стандартной форме. Каузальная форма.

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

1) Формулы А и Б равносильны;

2) Формула Б удовлетворяет следующим условиям:

a. Используются логические операции НЕ, И, ИЛИ, при этом отрицание применяется только в атомарных формах;

b. Операции применения квантеров следуют за операциями алгебры высказывания.

3) … форма включается в себя префикс, образованный квантерами всеобщности и существования и матрицу, под которой понимается формула не содержащая квантификацию.

, где Q – это один из квантеров всеобщности существования, а А – это формула не имеющая квантеров.

Пример:

Приведение логики предикатов к скалемовской форме призвано обеспечить дальнейшее упрощение логических представлений и облегчить введение машинных процедур в логику предикатов.

Отправной точкой скалемизации является предваренная нормальная форма.

Цель скалемизации – исключение квантера существования.

Каузальной формой называется такая скалемовская форма, матрица которой приведена к конъюнктивной нормальной форме.

Любая скалемовская форма допускает эквивалентную каузальную форму.