Логічне програмування

Логічне програмування можна розглядати як контрольований висновок. Важливою концепцією у логічному програмуванні є розділення програм на їх логічний компонент і їх компонент управління. З чистими логічними мовами програмування, тільки логічний компонент визначає отримані рішення. Компонент управління може бути змінений для забезпечення альтернативних способів виконання логічної програми. Це поняття зафіксовано гаслом: Алгоритм = Логіка + Управління. Де «Логіка» являє собою логічну програму, а «Контроль» являє собою різні стратегії доказу теорем.[3]

У спрощеному пропозиціональному випадку, коли логічна програма і атомна мета верхнього рівня не містять змінних, зворотне міркування визначає дерево and-or, яке являє собою простір для пошуку рішення завдання. Мета верхнього рівня — корінь дерева. Для будь-якого вузла у дереві і будь-якої пропозиції, головка якого збігається з вузлом, існує набір дочірніх вузлів, відповідних підцілях в тексті пропозиції. Ці дочірні вузли групуються разом «і». Альтернативні набори дітей, відповідні альтернативні способи вирішення вузла, групуються разом «або».

Будь-яка пошукова стратегія може використовуватися для пошуку цього простору. У Prolog використовується послідовна стратегія «назад-у-перших», зворотне трасування, в якій одночасно розглядається тільки одна альтернатива і одна підціль. Можливі також інші стратегії пошуку, такі як паралельний пошук, інтелектуальний відкат або кращий початковий пошук для пошуку оптимального рішення.

У більш загальному випадку, коли змінні спільного використання підцілей можуть використовуватися, можна використовувати інші стратегії, такі як вибір найбільш підходящої підцілі або достатнього примірника, так що застосовується тільки одна процедура. Такі стратегії, які використовуються, наприклад, при паралельному логічному програмуванні.

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

${\displaystyle H:-A1,...,An,notB1,...,Bn.}$

читається декларативно як логічне вираження:

${\displaystyle H,ifA1...An,notB1...,Bn.}$

де H та всі ${\displaystyle Ai}$ і ${\displaystyle Bi}$ — атомні формули. Заперечення негативних літералах, а не ${\displaystyle Bi}$, зазвичай називається «запереченний збій», оскільки в більшості реалізацій показано негативна умова, а не ${\displaystyle Bi}$ , показуючи, що позитивна умова ${\displaystyle Bi}$ не виконується. Наприклад:

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 був спочатку прив'язаний (зверніть увагу, що стандартний Пролог виконує цілі зліва направо).

Логічний статус заперечення як невдачі, так і залишився невирішеним, поки Кейт Кларк [1978] показали, що при певних природних умовах, це правильне (а іноді і повне) виконання класичного заперечення щодо завершення програми. Завершення приблизно збігається з набором всіх пропозицій програми, з тим же предикатом на лівій стороні, скажімо: H :- Body₁.

…

H :- Body_k.

Визначення предиката

H iff (Body₁ or … or Body_k)

де «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.

Поняття завершення тісно пов'язано з семантикою опису Маккарті для аргументації за замовчуванням і закритим світовим припущенням.

В якості альтернативи семантики завершення, заперечення як невдача може інтерпретуватися епістемічно, як і в семантиці стійких моделей та у відповідь множин програмування. У цій інтерпретації (${\displaystyle Bi}$) не означає буквально, що ${\displaystyle Bi}$ не відома або не враховується. Епітимічна інтерпретація має перевагу, що її можна комбінувати дуже просто з класичним запереченням, як у «розширеному логічному програмуванні», для формалізації таких фраз, як «протилежне не можна показати», де «навпаки» є класичним запереченням і «навпаки не може бути показаним» є епістичною інтерпретацією заперечення як невдачі.

Той факт, що пропозиції Хорна можуть бути дані процедурної інтерпретацією, і навпаки, що процедури усунення мети можна зрозуміти як пропозиції Хорна + зворотнє міркування означає, що логічні програми об'єднують декларативні і процедурні представлення знань. Включення заперечення як відмови означає, що логічне програмування є свого роду немонотонною логікою.

Попри свою простоту порівняно із класичною логікою, ця комбінація пропозицій Хорна і заперечення невдачі виявилася напрочуд виразним. Наприклад, він забезпечує природне подання для здорового глузду законів причини і слідства, а формалізується як ситуаційне числення та числення подій.Було також показано, що він цілком природно відповідає напівформальній мові законодавства. Зокрема, Праккен і Сартор кредитують подання Британського закону про громадянство як логічної програми будучи «надзвичайно впливовим для розробки обчислювальних уявлень законодавства, показуючи, як логічне програмування дозволяє інтуїтивно привабливими уявленнями, які можуть бути безпосередньо розгорнуті для створення автоматичних висновків».

Абдуктивне логічне програмування — це розширення нормального логічного програмування, яке дозволяє деяким предикатам, оголошеним як предикати, бути «відкритими» або невизначеними. Речення в логічній програмі абдуктивної логіки має вигляд:

${\displaystyle H:-B1,...,Bn,A1,...,An.}$

де H — атомна формула, яка не є неприводимою, всі ${\displaystyle Bi}$ є текстовими значеннями, предикат яких не є неприводимим, а ${\displaystyle Ai}$ — атомними формулами, предикат яких є неприводимим. Неприводимі предикати можуть бути обмежені обмеженнями цілісності, які можуть мати форму:

${\displaystyle false:-B1,...,Bn.}$

де ${\displaystyle Bi}$ — довільні літерали (визначені або неприводимі, а також атомні або негативні). Наприклад:

canfly(X) :- bird(X), normal(X).
false :-  normal(X), wounded(X).
bird(john).
bird(mary).
wounded(john).

де нормаль предиката є неприводимою.

Рішення проблем досягається шляхом виведення гіпотез, що виражаються в термінах відтворюваних предикатів, як рішень розв'язуваних завдань. Цими проблемами можуть бути або спостереження, які необхідно пояснити (як у класичних абдуктивних міркуваннях), так і цілі, які необхідно вирішити (як у звичайному логічному програмуванні). Наприклад, гіпотеза нормальна (mary) пояснює наглядову метелика (mary) . Більше того, та ж сама гіпотеза тягне за собою єдине рішення X = mary мета знайти щось, що може літати:

: -  canfly ( X ).

Логічне програмування абдукції було використано для діагностики несправностей, планування, обробки природної мови і машинного навчання. Він також використовувався для інтерпретації Заперечення як Відмова як форми абдуктивного міркування.

Оскільки математична логіка має давню традицію розрізнення між мовою об'єктів і метамовою, логічне програмування також дозволяє метарівневе програмування. Найпростіша металогічна програма — це так званий мета-інтерпретатор «ванілі»:

solve(true).
    solve((A,B)):- solve(A),solve(B).
    solve(A):- clause(A,B),solve(B).

де true являє собою порожню кон'юнкцію, а пропозиція (A, B) означає, що існує пропозиція рівня об'єкта форми A: — B.

Метаномічне програмування дозволяє комбінувати уявлення об'єктів і метарівнів, як на природній мові. Він також може використовуватися для реалізації будь-якої логіки, яка задається за допомогою правил виведення . Metalogic використовується в логічному програмуванні для реалізації метапрограм, які маніпулюють іншими програмами, базами даних, базами знань або аксіоматичними теоріями в якості даних.

Основна стаття: Логічне програмування з обмеженнями

Логічне програмування з обмеженнями поєднує в собі логічне програмування логіки Horn з рішенням обмеження . Він розширює пропозиції Хорна, дозволяючи деяким предикатам, оголошеними предикатами обмеження, зустрічатися як літерали в сукупності статей. Логічна програма обмеження являє собою набір пропозицій виду:

${\displaystyle H:-C1,...,Cn\lozenge B1,...,Bn.}$

де H та всі ${\displaystyle Bi}$- атомні формули, а ${\displaystyle Ci}$ — обмеження. Декларативно такі положення розглядаються як звичайні логічні наслідки: H, якщо ${\displaystyle G1...Gn|B1...Bn.}$

Однак, у той час як предикати є в главах розділів і визначаються програмою логіки обмежень, предикати обмеження зумовлені певною теоретико-просторовою структурою або теорією.

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

Наступна логічна програма обмеження являє собою іграшкову тимчасову базу даних історії Джона як вчителя:

teaches(john, hardware, T) :- 1990 ≤ T, T < 1999.
teaches(john, software, T) :- 1999 ≤ T, T < 2005.
teaches(john, logic, T) :- 2005 ≤ T, T ≤ 2012.
rank(john, instructor, T) :- 1990 ≤ T, T < 2010.
rank(john, professor, T) :- 2010 ≤ T, T < 2014.

Тут ≤ та < — предикати обмеження, з їх звичайною передбачуваною семантикою. Наступне речення мети запитує базу даних, щоб дізнатися, коли Джон викладав логіку і був професором:

:- teaches(john, logic, T), rank(john, professor, T).

Рішенням є : 2010 ${\displaystyle \leq }$T, T ${\displaystyle \leq }$2012.

Логічне програмування обмежень використовувалося для вирішення проблем у таких галузях, як цивільне будівництво, машинобудування, цифрова електроніка, автоматизоване планування та диспетчеризація, управління повітряним рухом і фінанси. Він тісно пов'язаний з абдуктивним логічним програмуванням.

Основна стаття: паралельне логічне програмування

Паралельне логічне програмування об'єднує концепції логічного програмування з паралельним програмуванням. Його розвиток отримав великий поштовх у 1980-х роках за його вибором для мови системного програмування японського проекту п'ятого покоління (FGCS).

Паралельна логічна програма являє собою набір захищених диз'юнктів Горна форми:

${\displaystyle H:-G1,...,Gn|B1,...,Bn.}$

Кон'юнкція ${\displaystyle G1,...,Gn}$ називається захистом пропозиції, а | є оператором зобов'язання. Декларативно охоронювані положення Горна читаються як звичайні логічні наслідки: H, якщо ${\displaystyle G1...Gn|B1...Bn.}$

Тим не менш, процедурно, коли є кілька пропозицій, голови H яких відповідають заданої мети, тоді всі параграфи виконуються паралельно, перевіряючи, чи перебувають їх гвардії ${\displaystyle G1,...,Gn}$ . Якщо огорожі більш ніж однієї пропозиції зберігаються, то в один з пропозицій робиться рішучий вибір, а виконання виконується з допомогою підцілей ${\displaystyle B1,...,Bn}$ вибраної пропозиції. Ці підцілі можуть також виконуватися паралельно. Таким чином, паралельне логічне програмування реалізує форму "не піклується про недетермінізм", а не «не знає недетермінізм».

Наприклад, наступна паралельна логічна програма визначає предикат shuffle (Left, Right, Merge) , який можна використовувати для перемішування двох списків вліво і вправо, об'єднуючи їх в один список Merge, який зберігає порядок двох списків вліво і вправо:

shuffle ([],  [],  []). 
shuffle ( Left ,  Right ,  Merge )  : - 
    Left  =  [ First  |  Rest ]  | 
    Merge  =  [ First  |  ShortMerge ], 
    shuffle ( Rest ,  Right ,  ShortMerge ). 
shuffle ( Left ,  Right ,  Merge )  : - 
    Right  =  [ First  |  Rest ]  |
    Merge  =  [ First  |  ShortMerge ], 
    shuffle ( Left ,  Rest ,  ShortMerge ).

Представляє [ ] порожній список, а [Head|Tail] представляє список з першим елементом Head, за яким слідує список Tail, як Prolog. (Зверніть увагу, що перше входження | у другому і третьому реченнях є конструктором списку, тоді як друге входження | є оператором зобов'язання.) Програма може використовуватися, наприклад, для перетасовки списків [ace, queen, king ] та [1, 4, 2], викликаючи пропозицію цілі:

shuffle([ace, queen, king], [1, 4, 2], Merge)

Програма буде детерміновано генерувати одне рішення, наприклад Merge = [ace, queen, 1, king, 4, 2] .

Можливо, паралельне логічне програмування засноване на передачі повідомлень і, отже, піддається тій же невизначеності, що і інші паралельні системи передачі повідомлень, такі як «Актори» (див. «Невизначеність при паралельному обчисленні»). Карл Хьюітт стверджував, що паралельне логічне програмування не засноване на логіці в його розумінні того, що обчислювальні етапи не можуть бути логічно виведені. Однак у паралельному логічному програмуванні будь-який результат завершального обчислення є логічним наслідком програми, і будь-який частковий результат часткового обчислення є логічним наслідком програми і залишкової мети (мережі процесів). Отже, невизначеність обчислень є наувазі, що не всі логічні наслідки програми можуть бути виведені.

Основна стаття: Логічне програмування паралельних обмежень

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

Основна стаття: Програмування індуктивної логіки

Індуктивне логічне програмування пов'язане з узагальненням позитивних і негативних прикладів у контексті фонових знань: машинне навчання логічних програм. Недавня робота в цій області, що поєднує логічне програмування, навчання і ймовірність, породила нову область статистичного реляційного навчання та ймовірнісного індуктивного логічного програмування .

F-logic розширює логічне програмування об'єктами та синтаксисом фреймів. Багато систем базуються на F-logic, включно з Flora-2 FLORID, і високомаштабовною комерційною системою Ontobroker.

Logtalk розширює Пролог підтримкою об'єктів, протоколів та інших понять ООП.

Логічне програмування на основі логіки в лінійній логіці призвело до створення мов логічного програмування, які значно виразніші, ніж ті, які засновані на класичній логіці. Програми пропозиції Horn можуть представляти тільки зміну станом шляху, зміни аргументів в предикаті. У лінійному логічному програмуванні можна використовувати лінійну логіку для підтримки зміни стану. Деякі ранні розробки логічних мов програмування на основі лінійної логіки включають LO [Andreoli & Pareschi, 1991], Lolli, [14] ACL, і Forum [Miller, 1996]. Форум забезпечує цілеспрямовану інтерпретацію всієї лінійної логіки.

Логіка транзакцій — це розширення логічного програмування з логічної теорією оновлень, що змінюють стан. Він має як теоретико-модельну семантику, так і процедурну. Реалізація підмножини логіки транзакцій доступна в системі Flora-2. Інші прототипи також доступні.

Деякі дослідники розширюють логічне програмування можливостями програмування вищого порядку успадкованих від логіки вищого порядку, таких як предикати-змінні. Реалізацією є наприклад розширення мови Пролог такі як HiLog and λProlog.