фикация является программой, то делать
Если специ фикация является программой, то делать больше нечего, и тысячи программистов можно заменить горсткой логиков. Причина того, что логическое программирование нетривиально, состоит в том, что чистая логика недостаточно эффективна для практического программирования, и поэтому есть этап, который должен быть пройден от научной теоретической логики до ее инженерных приложений в программировании.
В логическом программировании нет никаких «операторов присваивания», потому что управляющая структура единообразна для всех программ и состоит из поиска доказательства формулы. Поиск решений проблемы, конечно, не нов; новым является предположение, что поиск решений вычислительных проблем возможен в рамках общей схемы логических доказательств. Логика стала логическим программированием, когда было обнаружено, что, ограничивая структуру формул и способы, которыми делается поиск доказательств, можно сохранить простоту логических утверждений и тем не менее искать решения проблем эффективным способом. Перед объяснением как это делается, мы должны обсудить, как обрабатываются данные в логическом программировании.
17.2. Унификация
Хорновский клоз (Нот clause) — это формула, в которой с помощью конъюнкции («и»)элементарных формул выводится одиночная элементарная формула:
(s=>t)<=(t = tl||t2)^(S=>tl)
Логическое программирование основано на том наблюдении, что, ограничивая формулы хорновскими клозами, мы получаем правильное соотношение между выразительностью и эффективностью вывода. Такие факты, как t => t, являются выводами, которые ниоткуда не следуют, т. е. они всегда истинны. Вывод также называется головой формулы, потому при записи в инверсной форме оно появляется в формуле первым.
Чтобы инициализировать вычисление логической программы, задается цель:
"wof" => "Hello world"?
Машина вывода пытается сопоставить цель и вывод формулы.
