Подання задач у вигляді теорем

.

Зведення задач до підзадач

Цей метод нагадує спосіб подання задач в просторі станів. Суть його полягає в тім, що більша задача розбивається на кілька підзадач (декомпозиція), а ті у свою чергу, так само розбиваються на підзадачі. І так доти, поки не дійдемо до найменшої задачі, що може бути вирішена. Отриманий у такий спосіб граф (дерево рішень) містить вершину (початковий стан), з якої виходять дуги до підзадач, які так само є вершинами.

Вершини можуть бути двох типів:

§ Кон'юнктивні (вершини типу І), коли для рішення задачі потрібно вирішити всі вхідні в неї підзадачі.

§ Диз'юнктивні (вершини типу АБО), коли для рішення задачі досить вирішити хоча б одну вхідну в неї підзадачу задачі.

Розглянемо приклад обчислення невизначеного інтегралу

Дерево рішень можна представити в такому виді (з'єднані стрілки є кон'юнктивними вершинами:

Для подання задач у вигляді теорем використається мова логіки предикатів (наприклад, Пролог). Процес рішення задачі йде у такий спосіб:

Крок 1. Формується множина початкових істинних тверджень (аксіом).

Крок 2. Будується гіпотеза щодо результатів рішення задачі - цільове твердження.

Крок 3. Аксіоми комбінуються між собою на підставі правил виводу.

Крок 4. Перевіряється, чи не містить множина нових тверджень цільове твердження або його заперечення. Якщо містить, то процес рішення закінчується, інакше - отримана множина тверджень об'єднується з початковими аксіомами і процес повторюється.

Дата добавления: 2014-01-07