История
Идея использования языка логики предикатов первого порядка в качестве языка программирования возникла еще в 60-ые годы, когда создавались многочисленные системы автоматического доказательства теорем и основанные на них вопросно-ответные системы. Суть этой идеи заключается в том, чтобы программист не указывал машине последовательность шагов, ведущих к решению задачи, как это делается во всех процедурных языках программирования, а описывал на логическом языке свойства интересующей его области, иначе говоря, описывал мир своей задачи. Другие свойства и удовлетворяющие им объекты машина находила бы сама путем построения логического вывода. (В сущности, этот же подход реализуется и в функциональном программировании - лишь с тем уточнением, что речь в нем идет о свойствах функций. В связи с этим Дж. Робинсон предлагает назвать такой стиль программирования утвердительным).
Первые компьютерные реализации систем автоматического доказательства теорем появились в конце 50-х годов, а в 1965г. Робинсон предложил свой метод резолюций, который и по сей день лежит в основе большинства систем поиска логического вывода.
Робинсон пришел к заключению, что правила вывода, которые следует применять при автоматизации процесса доказательства при помощи компьютера, не обязательно должны совпадать с правилами вывода, используемыми человеком. Он обнаружил, что общепринятые правила вывода, например, правило modus ponens, специально сделаны “слабыми”, чтобы человек мог интуитивно проследить за каждым шагом процедуры доказательства. Правило резолюции более сильное, оно трудно поддается восприятию человеком, но эффективно реализуется на компьютере.
К концу 60-х годов выявились принципиальные трудности, препятствующие широкому применению таких систем. Главная проблема заключается в практической неэффективности известных методов построения логического вывода. Стремление обойти эту преграду привело к созданию различных линейных стратегий метода резолюций (в том числе стратегии SL-резолюции), которые, в сущности, являются прообразами современных интерпретаторов языка Пролог. В 1971г. один из авторов SL-резолюции Р. Ковальский прочитал несколько лекций по автоматическому доказательству теорем в лаборатории Искусственного интеллекта Марсельского университета. Работающий там А. Колмероэ и его коллеги вскоре поняли, каким образом можно использовать SL-резолюцию в качестве основы нового языка программирования. Так в 1972 году родился язык Пролог (“ПРОграммирование в терминах ЛОГики”), быстро завоевавший популярность во всем мире.
Терпеть не могу логики. Она всегда банальна и нередко убедительна.
Оскар Уайльд
