Розглянемо найдавніший зразок логічного висновку - силогізм:
«Все люди смертні. Сократ - людина. Отже, Сократ смертний ».
Як формалізувати такі умовиводи: навчити комп'ютер перевіряти їх правильність і автоматично генерувати подібні? Наш приклад складається з двох посилок «всі люди смертні», «Cократ - людина» і укладення «Cократ смертний», істинність якого випливає з істинності посилок. Запишемо першу посилку на «предикатні» мовою: «" x якщо x - людина, то x смертний ». На
підставі загальнозначущої формули "xP (x) ® P (a) логічно, опустивши в висловлюванні квантор", підставити замість х Сократа: «якщо Сократ - людина, то Сократ смертний». Поставимо поруч з отриманим висловлюванням другу посилку силогізму і отримаємо результат, який оформляється в наступному вигляді:
Якщо Сократ людина, то Сократ смертний. Сократ - людина.
У загальному випадку над рисою поміщаються логічні формули-посилки А, B. істинність яких гарантує істинність висновку З:
Cловесная запис правил логічного висновку звучить так: «З даних формул-посилок А, В слід формула-висновок С.» (Скорочено: А ÙВ ® С). При цьому вважається, що формула-висновок істинна принаймні при всіх таких значеннях предикатних, предметних і висказивательной змінних, при яких звертаються в істину все формули-посилки. Метод математичної індукції, оформлений як правило виведення, набуде вигляду:
Наведемо деякі правила виведення, що працюють в базах знань:
Розглянемо автоматизовану обробку знань. У системах штучного інтелекту знання - це інформація, на підставі якої
реалізується процес логічного висновку, що дозволяє зв'язати воєдино окремі фрагменти даних, а потім по цій послідовності фрагментів зробити висновок.
Розглянемо наступний приклад. У базі даних зберігаються відомості про співробітників установи Петрові, Іванові, Кузнецова, Яковлєва (надалі позначимо їх як П, І, К, Я).
Посадова ієрархія описується за допомогою двомісних предикатів:
PУK (П, І) означає, що Петров керує Івановим,
Отч (Y, X) означає, що Y звітує перед X.
У базі даних зберігаються три факти:
Далі описуються два правила виведення, які мають місце в аналізованої предметної області:
Потрібно перевірити запит користувача: чи повинен Яковлєв звітувати перед Івановим (тобто, зробити висновок отч (Я, І)).
У базі даних такого факту немає, проте предикат, що описує цікаву для нас зв'язок, зустрічається в правилах 1 і 2.
Застосовуючи правило 1 до факту 3, отримаємо формулу:
Застосовуємо до неї і фактом 3 правило виведення modus ponens:
так як вихідні вирази були правдиві, то висновок отч (Я, К) - новий факт - також є істинним.
Застосовуючи до отч (Я, К) і фактом 2: РУК (І, К) правило 2, отримаємо формулу:
вказує на відповідь отч (Я, І), який однак, треба ще перевірити. Для цього пов'язуємо факт 2 і отч (Я, К) правилом «введення кон'юнкції»:
і нарешті, застосовуючи modus ponens, обгрунтовуємо результат
дає ствердну відповідь на запит, чи дійсно Яковлєв звітує перед Івановим.