Принципы функционирования и способы реализации механизма логического вывода в ЭС

Механизм логического вывода в большинстве ЭС реализован по принципу опровержения резолюции.

•  Обобщенное правило вывода.

, где α и β – произвольные формулы логики предикатов. Запись означает: « α и β – утверждения, α влечет за собой β. Тогда при выполнении α, которое влечет за собой β, вытекакет и β».

•  Правило резолюции.

Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая – его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания.

или

•  Унификация.

Подстановка и связывание переменных для выполнения утверждения.

Синтаксис логики предикатов с использованием метаязыка Бекуса-Наура

Формула → Атом|

Предложение|

Предложение Связка Предложение|

Квантор (Переменная,..., Переменная) Предложение|

Предложение|

(Предложение)

Атом → Предикатный символ (Терм, Терм)|

Терм = Терм

Терм → Функциональный символ (Терм,..., Терм)|

Константа|

Переменная

Связка →

Квантор →

Константа → строка символов, начинающаяся с прописной буквы

Переменная → строка символов, начинающаяся со строчной буквы

Предикатный символ → строка символов, начинающаяся со строчной буквы

Функциональный символ → строка символов, начинающаяся со строчной буквы