Логі́чне програмува́ння — парадигма програмування, а також розділ дискретної математики, що базується на використанні логіки для опису проблем і пошуку їх рішень. Логічне програмування засноване на теорії математичної логіки. Найвідомішою мовою логічного програмування є Prolog, що є за своєю суттю універсальною машиною виводу, що працює в припущенні замкненості системи фактів.
Першою мовою логічного програмування була мова Planner, в якій була закладена можливість автоматичного виведення результату з даних і заданих правил перебору варіантів. Planner використовували для, зниження вимог до обчислювальних ресурсів (за допомогою методу пошуку з поверненням) і для виведення фактів без активного використання стеку. Потім була розроблена мова Prolog, яка не вимагала плану перебору варіантів і була, в цьому сенсі, спрощенням мови Planner.
На основі ідей Planner були створені такі мови логічного програмування, як: QA-4, Popler, Conniver і QLISP. Мови програмування Mercury, , Oz і були створені на основі Prolog. На основі мови Planner було розроблене також декілька альтернативних мов логічного програмування, не заснованих на методі пошуку з поверненням, наприклад, Ether.
Історія
Використання математичної логіки для представлення і виконання комп'ютерних програм також є властивістю лямбда-числення, розробленого Алонзом Черч в 1930-х роках. Однак, першим запропонував використовувати кон'юнктивну нормальну форму логіки для представлення комп'ютерних програм — Корделл Грін. Було використано аксіоматизацію підмножини LISP разом з представленням відношення вводу-виводу для обчислення відношення шляхом моделювання виконання програми в LISP. З іншого боку, мова Absys, розроблена Фостером і Елкоком, використовувала комбінацію рівнянь і лямбда-числення у вигляді тверджень без обмежень на порядок виконання операцій.J.M. Foster and E.W. Elcock. ABSYS 1: An Incremental Compiler for Assertions: an Introduction, Machine Intelligence 4, Edinburgh U Press, 1969, pp. 423–429
Логічне програмування в нинішньому вигляді можна простежити до дискусій в кінці 1960-х і початку 1970-х років про порівняння декларативного і процедурного представлення знань в штучному інтелекті. Прихильники декларативного представлення, працювали в Стенфорді, пов'язані з Джоном Маккарті, і , а також в Единбурзі з Джоном Аланом Робінсоном (академічним гостем із Сіракузького університету), і Робертом Ковальські. Прихильники процедурного представлення були в основному зосереджені в Массачусетському технологічному інституті під керівництвом Марвіна Лі Мінського та Сеймура Пейперта.
Хоча Planner був заснований на методах доведення логіки, розроблений Карлом Хьюіттом в Массачусетському технологічному інституті, він став першою мовою, що з'явилася в рамках цієї процесуалістичної парадигми.Planner показував шаблонне звернення процедурних планів від цілей (наприклад, метаскорочення або зворотний ланцюжок) і від тверджень (тобто прямий вивід). Найбільш впливова реалізація Planner була підмножиною під назвою Micro-Planner, реалізованого , і Террі Виноградом. Він був використаний для реалізації програми WinRED з вивченням природної мови SHRDLU, яка була орієнтиром в той час. Щоб впоратися з дуже обмеженими системами пам'яті, Планувальник використовував структуру управління зворотним трасуванням, щоб одночасно зберігати тільки один можливий шлях обчислення. Планувальник привів до появи мов програмування таких як: QA-4, Popler, Conniver, QLISP і паралельні мови Ether.
Гейс і Ковальський в Единбурзі намагалися узгодити логічний підхід декларативного підходу до подання знань з процедурних підходів Планера. Hayes (1973) розробив екваціональну мову, Golux, в якому різні процедури можуть бути отримані шляхом зміни поведінки доведення теорем. Ковальський, з іншого боку, розробив SLD-резолюція, варіант SL-резолюції і показав, як він розглядає наслідки «процедури скорочення мети». Ковальський співпрацював з в Марселі, який розробив ці ідеї при розробці та впровадженні мови програмування Prolog.
була створена для підтримання логічного програмування в 1986 році.
У Prolog з'явилися мови програмування , , , Mercury, Oz, , , XSB і , а також безліч мов , мови і Datalog.
Формальна логіка як основа логічного програмування. Метод резолюцій
Для будь-якої системи логічного програмування характерним є те, що для виконання програми (побудови виведення результату) використовується вмонтована система автоматичного пошуку. Механізм пошуку логічного висновку Prolog-у бере свій початок від методу резолюцій Робінсона. Правило резолюції виведення логічного висновку працює наступним чином: дві фрази можуть резольвувати між собою, коли одна з них має позитивний, а друга — негативний літерал з одним і тим самим позначенням предиката та однаковою кількістю аргументів і в разі, якщо аргументи обох літералів можуть бути уніфіковані (погоджені). Наприклад, фраза P(a, b) o Q(c, d) і фраза Q(c, d) o R(b, c) дають резольвенту P(a, b) o R(b, c). Якщо ж аргументом відношення є змінна, то вона уніфікується з константою, а резольвента буде мати дану константу на місцях попереднього розташування змінної. Розглянемо дві фрази спеціального вигляду: Р(а) — висловлювання без умови і oP(а) — умова без висловлювання. Наявність цих двох фраз в одній теорії є суперечністю. Якщо вони резольвуються між собою, тоді отримана резольвента називається порожньою фразою. Якщо при резолюції двох фраз, що входять до складу теорії, отримується порожня фраза, то теорія буде непослідовною.
Концепції
Логіка і управління
Логічне програмування можна розглядати як контрольований висновок. Важливою концепцією у логічному програмуванні є розділення програм на їх логічний компонент і їх компонент управління. З чистими логічними мовами програмування, тільки логічний компонент визначає отримані рішення. Компонент управління може бути змінений для забезпечення альтернативних способів виконання логічної програми. Це поняття зафіксовано гаслом: Алгоритм = Логіка + Управління. Де «Логіка» являє собою логічну програму, а «Контроль» являє собою різні стратегії доказу теорем.
Рішення проблем
У спрощеному пропозиціональному випадку, коли логічна програма і атомна мета верхнього рівня не містять змінних, зворотне міркування визначає , яке являє собою простір для пошуку рішення завдання. Мета верхнього рівня — корінь дерева. Для будь-якого вузла у дереві і будь-якої пропозиції, головка якого збігається з вузлом, існує набір дочірніх вузлів, відповідних під цілі в тексті пропозиції. Ці дочірні вузли групуються разом «і». Альтернативні набори дітей, відповідні альтернативні способи вирішення вузла, групуються разом «або».
Будь-яка пошукова стратегія може використовуватися для пошуку цього простору. У Prolog використовується послідовна стратегія «назад-у-перших», зворотне трасування, в якій одночасно розглядається тільки одна альтернатива і одна підмета. Можливі також інші стратегії пошуку, такі як паралельний пошук, інтелектуальний відхід або кращий початковий пошук для пошуку оптимального рішення.
У більш загальному випадку, коли змінні спільного використання під цілей можуть використовуватися, можна використовувати інші стратегії, такі як вибір найбільш підхожої під цілі або достатнього примірника, так що застосовується тільки одна процедура. Такі стратегії, які використовуються, наприклад, при .
Заперечення як відмова
Для більшості практичних додатків, а також для додатків, які вимагають немонотонного міркування в штучному інтелекті, логічні програми клаузули Хорна необхідно поширювати на звичайні логічні програми з негативними умовами. Положення в нормальній логічній програмі має вигляд:
читається декларативно як логічне вираження:
де H та всі і — атомні формули. Заперечення негативних літералах, а не , зазвичай називається «запереченний збій», оскільки в більшості реалізацій показано негативна умова, а не , показуючи, що позитивна умова не виконується. Наприклад:canfly(X) :- bird(X), not abnormal(X). abnormal(X) :- wounded(X). bird(john). bird(mary). wounded(john).Враховуючи мету знайти щось, що може літати::- canfly(X).Існує два рішення, які вирішують першу під цільну птицю (X), а саме X = john і X = mary. Друга під ціль не є ненормальним (john) для першого рішення, кандидату не вдається, бо поранений (john) досягає успіху отже і ненормальний (john) досягає успіху. Тим не менш, друга під ціль не є ненормальним (mary) для другого рішення, кандидат успішний, бо поранений (mary) але зазнає невдачу, а отже і ненормальний (mary) зазнає невдачі. Отже, X = mary — єдине рішення цілі.
Мікро-планувальник який було побудовано, називається «thnot», який при нанесенні на вираз повертає значення True, якщо (і тільки якщо) оцінка вираження завершується. Еквівалентний оператор зазвичай вбудований в сучасний «Пролог». Це зазвичай пишуться not(Goal) або \+ Goal , де Goal є (пропозиція) для програми. Цей оператор відрізняється від заперечення в логіці першого порядку: заперечення, наприклад \+ х == 1 завершується, коли змінна х зв'язана з атомом 1, але він досягає успіху у всіх інших випадках, у тому числі, коли x є неприв'язаний. Це робить міркування у Пролозі немонотонно: х = 1, \+ х == 1 і завжди зазнає невдачі, А \+ Х == 1, х = 1 може досягти успіху, прив'язки до 1 в залежності від x ,якщо x був спочатку прив'язаний (зверніть увагу, що стандартний Пролог виконує цілі зліва направо).
Логічний статус заперечення як невдачі, так і залишився невирішеним, поки Кейт Кларк показали, що при певних природних умовах, це правильне (а іноді і повне) виконання класичного заперечення щодо завершення програми. Завершення приблизно збігається з набором всіх пропозицій програми, з тим же предикатом на лівій стороні, скажімо: H :- Body1.
… H :- Bodyk. Визначення предиката H iff (Body1 or … or Bodyk)
де «iff» означає «якщо і тільки якщо». Написання завершення також вимагає явного використання предиката рівності і включення набору відповідних аксіом для рівності. Тим не менш, реалізація заперечення невдачею вимагає тільки if-половин визначень без аксіом рівності.
Наприклад, завершення вищенаведеної програми: canfly(X) iff bird(X), not abnormal(X). abnormal(X) iff wounded(X). bird(X) iff X = john or X = mary. X = X. not john = mary. not mary = john.
Поняття завершення тісно пов'язано з семантикою Маккарті для аргументації за замовчуванням і .
В якості альтернативи семантики завершення, заперечення як невдача може інтерпретуватися епістемічно, як і в семантиці стійких моделей та у відповідь множин програмування. У цій інтерпретації () не означає буквально, що не відома або не враховується. Епітимічна інтерпретація має перевагу, що її можна комбінувати дуже просто з класичним запереченням, як у «розширеному логічному програмуванні», для формалізації таких фраз, як «протилежне не можна показати», де «навпаки» є класичним запереченням і «навпаки не може бути показаним» є епістичною інтерпретацією заперечення як невдачі.
Представлення знань
Той факт, що пропозиції Хорна можуть бути дані процедурної інтерпретацією, і навпаки, що процедури усунення мети можна зрозуміти як пропозиції Хорна + зворотне міркування означає, що логічні програми об'єднують декларативні і процедурні представлення знань. Включення заперечення як відмови означає, що логічне програмування є свого роду немонотонною логікою.
Попри свою простоту порівняно із класичною логікою, ця комбінація пропозицій Хорна і заперечення невдачі виявилася напрочуд виразним. Наприклад, він забезпечує природне подання для здорового глузду законів причини і слідства, а формалізується як ситуаційне числення та .Було також показано, що він цілком природно відповідає напівформальній мові законодавства. Зокрема, Праккен і Сартор кредитують подання Британського закону про громадянство як логічної програми будучи «надзвичайно впливовим для розробки обчислювальних уявлень законодавства, показуючи, як логічне програмування дозволяє інтуїтивно привабливими уявленнями, які можуть бути безпосередньо розгорнуті для створення автоматичних висновків».
Prolog