1.Логическое программирование- это направление в программировании, основанное на идеях и методах математической логики. Термин логическое программирование в литературе по информатике трактуется в широком и узком смысле.
В широком толковании ЛП включает круг понятий, методов, языков и систем, в основе которого лежит идея описания задачи с совокупностью утверждений на некотором логическом языке и получение решения задачи путём построения логического вывода в некоторой формальной дедуктивной системе. Классы формул, используемые для описания задач, методы вывода и модели вычислений, используемые для описания задач, методы вывода и модели вычислений, используемые в таких системах, очень разнообразные, поэтому различные их комбинации образуют специфические стили программирования: концептуальная, функциональная (аппликативная) и др.
Наибольшие практические результаты достигнуты в системах программирования, где в качестве логических программ используются специальные классы логических формул: хорновские дизъюнкты, а в качестве способа их использования применяются специальные методы логического вывода-варианты метода резолюции.
Программирование с использованием таких систем называется хорновским или резолюционным,но чаше всего - логическим программированием,перенося узкую трактовку термина на более широкое понятие.
Самыми известными системами такого рода являются реализации языка Prоlоg (программирование в терминах логики – Programming in logic). Рассмотрим основные идеи и понятие ЛП в узком смысле.
Неформально логическая программа описывает множество объектов, множество функций и отношения этих объектов. Строится логическая программа как набор утверждений об объектах, функциях и отношениях. Такое описание является статистическим и никакого вычислительного процесса не задает, т.е. можно считать, что это описание определяет БД в которой хранятся объекты и заданные на них функции и отношения, например, в виде графиков. К конкретному применению логической программы относится понятие запроса (цели) - например, каково значение функции заданной логической программой при данном значении аргумента. Вычисление ответа на запрос соответствует доказательству существования такого объекта. Провала, по которым проводятся вычисления, образуют процедурно-операционную семантику логической программы. Успехи языка Prolog обусловлены тем, что с одной стороны, с помощью используемых в них логических формул хорновских дизъюнктов - можно описать многие практические задания, а с другой - найдена простота интерпретации этих формул и построена достаточно эффективная реализация системы ЛП.
2.Правилав Prolog имеют вид:
m
где , - это атомы, атом называется заголовком, а атомы - телом правила. Тело может быть пустым (при m=0)- такие правила называются фактами.Атом имеет вид
Где - арный предикатный символ или имя отношения; - термы.
Терм - это либо имя переменной, либо константа, либо составной терм вида ,f - это n-арный функциональный символ.
Функции, задаваемые при логическом программировании, представляются в виде отношений - n-местная функция у =f (X1,X2…Xn) представляется в виде (n+1)- местного отношения вида F(X1,X2…Xn,Y).
Запрос(это цель) имеет вид: С1,С2...Сr, где r>= 0 и С1, C2…Сr- атомы.
Каждое правило допускает логическую и процедурную интерпретацию (в семантике). Логическая интерпретация правила - «истинность A0 следует из истинности а1 .и истинности A2, и истинности Аm» или «Ао истинно, если истинны А1,A2, Am».
Т.о. правила рассматриваются, как формулы языка логики предикатов вида:
Здесь - квантор общности.
- логическая связка «И».
- логическая связка «если, то»
В Прологе данные, формулы записываются в обратную сторону и используются другие обозначения:
- обозначается "," (запятой) или словом and . v - ";"(точка с запятой) или «оr».
- "I" или «: -» или if.
Формула с использованием связок логич. программ. может быть преобразована в эквивалентную, но имеющую связки (НЕ) и (ИЛИ) , формулу вида:
(т > 0).
Такие формулы и называются хорновскими дизъюнкциями, а стиль программирования хорновским.
3.Метод резолюции- получив на вход логическую программу с присоединенными к ней запросами в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом "а". Если это ему удаётся, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюции и помощью двух правил:
Правило резолюции или правило склейки,которое во время работы вызывает процедуру унификации — сопоставления.
Унификация- это процесс, на вход которого поступает два терма и для них находится унификатор.
Унификаторомдвух термов называется подстановка, которая делает термы одинаковыми и если унификатор существует, то термы называются унифицируемыми и для них отыскивается наиболее общий унификатор, если нет - процедура унификации сообщает об отказе.
Правило резолюции.Позволяет из дизъюнктов:
Получить новый дизъюнкт:
Здесь - наиболее общий унификатор термов t и s, обеспечивает их равенство и означает, что все подстановки унификатора выполнены для всех атомов, входящих в дизъюнкты D1и D2. Дизъюнкты D1 и D2называются родителями дизъюнкта D. В дизъюнкте D отсутствует пара
, при этом () = () и пара является тавтологией (тождественно истинной) и может быть удалена из дальнейших вычислений и выполняет правило резолюции.
Правило склейкипозволяет из дизъюнкта A(t)A(s)получить дизъюнкт, т.е. осуществляется склеивание одинаковых атомов, полученных после унифицирующей подстановки .
m 
, - это атомы, атом 
называется заголовком, а атомы 
- телом правила. Тело может быть пустым (при m=0)- такие правила называются фактами.Атом имеет вид
- арный предикатный символ или имя отношения; 
- термы.
,f - это n-арный функциональный символ.
С1,С2...Сr, где r>= 0 и С1, C2…Сr - атомы.
- квантор общности.
- логическая связка «И».
- логическая связка «если, то»
(т > 0).
- наиболее общий унификатор термов t и s, обеспечивает их равенство и означает, что все подстановки унификатора выполнены для всех атомов, входящих в дизъюнкты D1и D2. Дизъюнкты D1 и D2называются родителями дизъюнкта D. В дизъюнкте D отсутствует пара
, при этом (
) = (
) и пара является тавтологией (тождественно истинной) и может быть удалена из дальнейших вычислений и выполняет правило резолюции.
A(s)
получить дизъюнкт
, т.е. осуществляется склеивание одинаковых атомов, полученных после унифицирующей подстановки 
.