Правила вывода. Унификация

Назначение правил вывода: на основе множества ППФ получить новые корректные ППФ. Известно большое количество правил вывода, среди которых наиболее часто применяемыми являются следующие правила:

Правило вывода 1: . Модус поненс - операция, создающая ППФ W2 из ППФ вида W1 и W1 W2. Это правило интерпретируется так: если истинно утверждение , и из следует , то утверждение тоже истинно.

Правило вывода 2: Транзитивность оператора импликации.

Правило вывода 3: Слияние утверждений и .

Правило вывода 4: Резолюция двух ППФ.

Правило вывода 5: Специализация - создает ППФ W(А) из ППФ "(x)W(х),

где А - любой символ константы.

Унификация – процесс поиска подстановочных термов на место переменных. Обозначение подстановок: , где - новая переменная, - заменяемая переменная. - подстановка s применяется к каждому элементу множества ППФ . Назначение унификации – приведение ППФ к заданному виду.

Множество ППФ называется унифицируемым, если существует подстановка s такая, что . Такая подстановка называется унификатором. Применение унификатора сворачивает унифицируемое множество в один элемент.