Page 41 - 6109

вважаємо істинними, називають аксіомами та гіпотезами, а ті твердження, що з
них випливають, – теоремами.
Як уже зазначалося раніше, звістка про те, що цифрові комп'ютери
можуть автоматично доводити теореми, у 60-ті роки спричинила бурхливий
сплеск ентузіазму. Перші спроби знайти загальний алгоритм для вирішення
задачі автоматизації дедуктивних побудов простежуються в роботах Лейбніца,
Пеано, Гільберта. Центральне місце серед сучасних методів автоматичного
доведення теорем займає метод резолюцій, запропонований Дж. Робінсоном у
1965 р. Використання цього методу виявилося ефективнішим, ніж класичне
виведення на основі modus ponens.
Оскільки числення предикатів є алгоритмічне нерозв'язним, метод ре-
золюцій дозволяє встановити, що деяка формула є теоремою, якщо вона
насправді є теоремою. Для формул, що не є теоремами, метод резолюцій може
працювати нескінченно довго. Саме на цій основі з'явилися ідеї, на яких
базуються мови логічного програмування. Одним з фундаментальних проривів
того часу було відкриття Дж. Робінсоном принципу аналізу та його
застосування до автоматичного доведення теорем. Аналіз – це правило
висновків, як одне твердження може випливати з іншого. Використовуючи
аналітичний принцип, ми можемо на основі аксіом довести теореми
стандартним шляхом з наших аксіом. Ми тільки маємо вирішити, до яких
тверджень їх застосувати, і відповідний висновок дістанемо автоматично.
Аналіз розроблено і для роботи з формулами у фразовій формі. Маючи ці
фрази, що пов'язані відповідним чином, він створить нову фразу, що буде
наслідком перших двох. Основна ідея – це те, що якщо одна й та сама часткова
формула зустрічається у правій частині однієї структури і в лівій частині іншої,
то фраза отримується з'єднанням двох фраз з вилученням дубльованих формул,
які з них випливають.
Метод резолюцій базується на правилі резолюцій.
Метод резолюцій – метод доведення того, що формула G є логічним
наслідком формул F 1, F 2,…, F n. Задача зводиться до перевірки виконуаності.
Тобто формула G є логічним наслідком формул F 1, F 2,…, F n тоді і тільки тоді
коли множина формул {F 1, F 2,…, F n, ~G} невиконувана. Таким чином, можна
відмітити, що метод резолюцій володіє такими особливостями:
– встановлює невиконуваність;
– оперує з дизюнктами.
Нагадаємо, що літералом ми називаємо атомарну формулу або її
заперечення, дизюнктом  дизюнкцію літералів. Диз’юнкт може складатися і із
одного літералу. В принципі можна дивитися , як на множину літералів, тобто
не розрізняємо дизюнкти, які отримуються один з одного шляхом

комутативності, асоціативності.
X  ~Y  X  X  ~Y
Крім того неохідності ввести поняття порожнього дизюнкта (немістить
літералів). Порожній дизюнкт  завжди хибний при будь-якій інтепритації,
тобто
F   , F   F

41