Для выполнения логической программы набор
Для выполнения логической программы набор логических формул (программа) и формула-цель, например:
"wor" =>"Hello world"?
предлагаются программной системе, которая названа машиной вывода, потому что она из одних формул выводит другие, являющиеся их следствием, пока проблема не будет решена. Метод логического вывода проверяет, можно ли доказать целевую формулу, исходя из аксиом, т.е. формул программы, которые приняты за истинные. Ответом может быть и «да», и «нет», что в логическом программировании называется «успехом» или «неуспехом». «Неуспех» мог быть получен из-за того, что цель не следует из программы, например, "wro" не является подстрокой "Hello world", или из-за неправильности программы, например, если мы пропустили одну из формул программы. Возможен и третий вариант, когда поиск машины вывода будет продолжаться без выбора того или иного ответа, и, так же как это может случиться с while-циклом в языке С, никогда не завершится.
Основные понятия логического программирования:
• Программа является декларативной и состоит исключительно из формул математической логики.
• Каждый набор формул для того же самого предиката (такого как «с») интерпретируется как процедура (возможно, рекурсивная).
• Конкретное вычисление определяется предложенной целью, т.е. формулой, о которой нужно выяснить, является ли она следствием программы.
• Компилятор является машиной вывода, которая по мере возможности ищет доказательство цели из программы.
Таким образом, каждую логическую программу можно прочитать двояко: как набор формул и как спецификацию вычисления. В некотором смысле, логическая программа — это минимальная программа. В разработке программного обеспечения вас обучают точно определять смысл программы перед попыткой ее реализовать, и для точной спецификации используется формальная нотация, обычно некоторая форма математической логики.
