![]() |
![]() |
Механизм логического вывода в большинстве ЭС реализован по принципу опровержения резолюции.
Обобщенное правило вывода.
, где α и β – произвольные формулы логики предикатов. Запись означает: « α и β – утверждения, α влечет за собой β. Тогда при выполнении α, которое влечет за собой β, вытекакет и β».
Правило резолюции.
Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая – его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого дизъюнкта и его отрицания.
или
Унификация.
Подстановка и связывание переменных для выполнения утверждения.
Формула → Атом|
Предложение|
Предложение Связка Предложение|
Квантор (Переменная,..., Переменная) Предложение|
Предложение|
(Предложение)
Атом → Предикатный символ (Терм, Терм)|
Терм = Терм
Терм → Функциональный символ (Терм,..., Терм)|
Константа|
Переменная
Связка →
Квантор →
Константа → строка символов, начинающаяся с прописной буквы
Переменная → строка символов, начинающаяся со строчной буквы
Предикатный символ → строка символов, начинающаяся со строчной буквы
Функциональный символ → строка символов, начинающаяся со строчной буквы
![]() |
![]() |