ПРИКЛАД ВИКОРИСТАННЯ АЛГОРИТМУ ПРОГРАМИ GPS

Розглянемо завдання в галузі формальної логіки [6, С. 296-302): знайти послідовність дозволених перетворень, що дозволяють перейти від формули (/?->-./*) л (-iR- ^ Q) (це і є вихідний об'єкт I ) до формули -1 (- PaQ) (кінцевий об'єкт Е). Дозволеними перетвореннями будемо вважати такі перетворення, що представляють собою, по суті, правила переписування одних рядків символів в інші:

Перетворення Про ₀ -О _ь дозволяється використовувати як для всієї формули в цілому, так і для окремих її частин, наприклад:

У першому випадку Про ₀ застосовуються до всієї перетворюється формулою, в другому - тільки до її частини, до подформуле -i -> (G л F).

Перетворення O _s - O _l2 дозволяється застосовувати тільки до всієї формулою в цілому, наприклад, допустимим є перетворення Про _н в наступних прикладах:

Неприпустимим є перетворення Про _н в прикладах:

Це зазначено перекресленням стрілок. У перетвореннях 0 _S - 0 _{] 2} стрілка => відрізняється від стрілки | => в перетвореннях 0 ₍ -0 ₂ . Подвійна стрілка <=> в Про ₀ -О ₇ означає, що допустимі обидва перетворення С1 | => С2 і С2 | => С1, наприклад, перетворення Про _ь , що має від4- »5 <=> -. 4aS, означає, що допустимі обидва перетворення:

Визначимо ті властивості (відмінності), за якими будемо порівнювати формули. Їх шість:

• - збільшення кількості букв (/),);
• - меншу кількість букв (Д ₂ );
• - число символів заперечення (Z),);
• - число інших зв'язок (Д,);
• - змінена розстановка дужок (Д ₅ );
• - змінений порядок букв (Ц);

Аналізуючи дії, які надають на ці відмінності перетворення Про ₀ -0 ₁₂ , можна побудувати наступну таблицю залежностей.

Таблиця 2

Таблиця залежностей в завданню перетворення формул

Початкова вершина дерева підзадач відповідає вихідній задачі Т (/,?), Або T {(R ^ P) л -, (-, /> л {?)).

Мал. 12

Початковий фрагмент дерева підзадач для поставленої задачі представлений на рис. 12.

На ньому в вершинах дерева позначені формули, а навпаки ребер графа позначені оператори перетворення, що призводять до відповідних формулах. Виділені ребра вказують на вирішальне поддерево. Многоточия відповідають недобудованим частинах дерева.