их операторів, операторів циклу і т. д. Вона являє собою модель фрагмента предметної області, про який йде мова в задачі. І рішення задачі записується не в термінах комп'ютера, а в термінах предметної області розв'язуваної задачі, в дусі модного зараз об'єктно програмування.
Пролог дуже добре підходить для описи взаємин між об'єктами. Тому Пролог називають реляційним мовою. Причому "Реляційних" Прологу значно могутніша і розвинута, ніж "Реляційних" мов, що використовуються для обробки баз даних. Часто Пролог використовується для створення систем управління базами даних, де застосовуються дуже складні запити, які досить легко записати на Пролозі. p> У Пролозі дуже компактно, по порівняно з імперативними мовами, описуються багато алгоритми. За статистикою, рядок вихідного тексту програми мовою Пролог відповідає чотирнадцяти рядкам вихідного тексту програми на імперативний мовою, вирішальному ту ж задачу. Пролог-програму, як правило, дуже легко писати, розуміти і налагоджувати. Це призводить до того, що час розробки додатка мовою Пролог у багатьох випадках на порядок швидше, ніж на імперативних мовах. У Пролозі легко описувати й обробляти складні структури даних. p> Прологу властивий ряд механізмів, якими не володіють традиційні мови програмування: зіставлення з зразком, висновок з пошуком і поверненням. Ще одна істотна відмінність полягає в тому, що для зберігання даних в Пролозі використовуються списки, а не масиви. У мові відсутні оператори присвоювання й безумовного переходу, покажчики. Природним і найчастіше єдиним методом програмування є рекурсія. Тому часто виявляється, що люди, які мають досвід роботи на процедурних мовах, повільніше освоюють декларативні мови, ніж ті, хто ніколи раніше програмуванням не займався, так як Пролог вимагає іншого стилю мислення, відмови від стереотипів імперативного програмування.
Фрази Хорна (Horn clause) являють собою підмножину фраз, які містять тільки один позитивний літерал. У загальному вигляді фраза Хорна представляється виразом
У мові PROLOG ця ж фраза записується в такому вигляді:
р: - q1, ..., qn. Така фраза інтерпретується таким чином:
"Для всіх значень змінних у фразі p істинно, якщо істинні q1 і ... і qn ",
тобто пара символів ": -" читається як "якщо", а коми читаються як "і".
PROLOG - це не зовсім звичайний мова програмування, в якому програма складається в основному з логічних формул, а процес виконання програми являє собою доказ теореми певного виду.
Фраза у формі
р: - q1, ..., qn.
може розглядатися в якості процедури. Така процедура передбачає наступний порядок виконання операцій. p> (1) Літерал мети зіставляється з літералом р (уніфікується з р), який називається головою фрази.
(2) Хвіст фрази ql ..., qn конкретизується підстановкою значень змінних (або уніфікаторів), сформованих в результаті цього зіставлення.
(3) Конкретизовані терми хвостовій частині утворюють потім безліч підцілей, які можуть бути використані іншими процедурами.
Таким чином, зіставлення (або уніфікація) грає ту ж роль, що і передача параметрів функції в інших, більш звичних мовах програмування.
Наприклад, розглянемо набір фраз мови PROLOG, представлених у лістингу 1. Припустимо, що a, b і з - якісь блоки в світі блоків. Дві перші фрази затверджують, що а перебуває на (on) b, a b знаходиться на (on) с. Третя фраза стверджує, що X знаходиться вище (above) Y, якщо X знаходиться на (on) Y. Четверта фраза стверджує, що X знаходиться вище (Abov e) Y, якщо існує якийсь інший блок Z, розміщений на (on) Y, і X знаходиться вище (above) Y.
Лістинг 1. Проста програма мовою PROLOG, визначає ставлення
on (на)
on (а, b).
on (b, с).
above (X, Y): - on (X, Y).
above (X, Y): - on ( Z, Y),
above (X, Z).
Очевидно, що від програми потрібно вивести мета above (а, с) з цієї множини фраз. Процес формулювання вираження мети включає обробку двох процедур above і використання двох фраз on. У мові PROLOG використовується "інтерпретація фраз Хорна для вирішення проблем "Фундаментальний метод доведення теорем, на якому базується PROLOG, називається спростуванням резолюцій (resolution refutation).
В
3.3 Принцип резолюцій
Ми намагаємося спростити синтаксис обчислення таким чином, щоб зменшити кількість правил впливу, необхідне для доведення теорем. Замість дюжини або більше правил, які використовуються при доказі теорем вручну, системи автоматичного докази для фразових форм використовують єдине правило виводу - принцип резолюцій, - вперше описане Робінсоном ([Robinson, 1965]).
Розглянемо наступний приклад з числення висловів. Надалі прописними літерами Р, Q, R, ... будуть позначатися окремі фрази, а малими грецькими U, ф і ВЈ - проп...
