Базис логического программирования

Алгоритмы и программы

Алгоритм — это точное предписание, определяющее вычислительный процесс, идущий от варьируемых исходных данных к искомому результату

Алгоритм — это конечный набор правил, который определяет последовательность операций для решения конкретного множества задач и обладает пятью важными чертами: конечность, определённость, ввод, вывод, эффективность

Реку́рсия — метод определения класса объектов или методов предварительным заданием одного или нескольких (обычно простых) его базовых случаев или методов, а затем заданием на их основе правила построения определяемого класса, ссылающегося прямо или косвенно на эти базовые случаи.

Факториал целого неотрицательного числа n (обозначается n!) определяется как

Базис логического программирования - student2.ru при n > 0 и n! = 1 при n = 0

В состав машины Тьюринга входит бесконечная в обе стороны лента (возможны машины Тьюринга, которые имеют несколько бесконечных лент), разделённая на ячейки, и управляющее устройство, способное находиться в одном из множества состояний. Число возможных состояний управляющего устройства конечно и точно задано.

Управляющее устройство может перемещаться влево и вправо по ленте, читать и записывать в ячейки ленты символы некоторого конечного алфавита. Выделяется особый пустой символ, заполняющий все клетки ленты, кроме тех из них (конечного числа), на которых записаны входные данные.

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

domains
c=char
i=integer
s=i*
database
a(c)
b(c)
d(s)
mp(i,c,c,i)
predicates
t(c,s)
mz(i,s)
m(i,i,c)
app(s,s,s)
r(c)
z(c)
rab
rba
p(c)
clauses
m(V,E,D):-r(X),retract(mp(V,X,D,E)),
asserta(mp(V,X,D,E)),!.
p(D):-D=' ',z(D),!.
p(D):-D='1',z(D),!.
p(D):-D='P',rba,!.
p(D):-D='L',rab,!.
p(D):-D='K',!.
t(V,L1):-retract(d(L0)),mz(M,L0),
m(M,E,V),p(V),app([E],L0,L1),
asserta(d(L1)).
mz(M,[M|_]).
app([],X,X):-!.
app([A|L1],L2,[A|L3]):-!,app(L1,L2,L3).
r(X):-retract(b(X)),asserta(b(X)),!.
z(X):-retract(b(_)),asserta(b(X)),!.
rab:-retract(a(X)),asserta(b(X)),!.
rba:-retract(b(X)),asserta(a(X)),!.
goal
asserta(mp(1,'1',' ',1)),assertz(mp(1,'*','K',1)),
assertz(mp(1,' ','P',2)),assertz(mp(2,'1','P',2)),
assertz(mp(2,'*','P',3)),assertz(mp(3,'1',' ',3)),
assertz(mp(3,'*','L',8)),assertz(mp(3,' ','P',4)),
assertz(mp(4,'1','P',4)),assertz(mp(4,'*','P',5)),
assertz(mp(5,'1','P',5)),assertz(mp(5,' ','1',6)),
assertz(mp(6,'1','L',6)),assertz(mp(6,'*','L',6)),
assertz(mp(6,' ','1',7)),assertz(mp(7,'1','P',3)),
assertz(mp(8,'1','L',8)),assertz(mp(8,'*','L',8)),
assertz(mp(8,' ','1',9)),assertz(mp(9,'1','P',1)),

asserta(b('1')),assertz(b('1')),
assertz(b('*')),assertz(b('1')),
assertz(b('1')),assertz(b('1')),
assertz(b('*')),assertz(b(' ')),
assertz(b(' ')),assertz(b(' ')),
assertz(b(' ')),assertz(b(' ')),
assertz(b(' ')),assertz(b(' ')),
L0=[1],asserta(d(L0)),
!,t(V,_),V='K',!,

retract(a(W)),write(".",W),
retract(a(W1)),write(".",W1),write("x"),
retract(b(Q)),write(" ",Q),fail.

Нормальные алгоритмы являются вербальными, то есть предназначенными для применения к словам в различных алфавитах. Определение всякого нормального алгоритма состоит из двух частей: определения алфавита алгоритма (к словам в котором алгоритм будет применяться) и определения его схемы. Схемой нормального алгоритма называется конечный упорядоченный набор т. н. формул подстановки, каждая из которых может быть простой или заключительной. Простыми формулами подстановки называются слова вида Базис логического программирования - student2.ru , где L и D — два произвольных слова в алфавите алгоритма (называемые, соответственно, левой и правой частями формулы подстановки). Аналогично, заключительными формулами подстановки называются слова вида Базис логического программирования - student2.ru , где L и D — два произвольных слова в алфавите алгоритма. При этом предполагается, что вспомогательные буквы Базис логического программирования - student2.ru и Базис логического программирования - student2.ru не принадлежат алфавиту алгоритма (в противном случае на исполняемую ими роль разделителя левой и правой частей следует избрать другие две буквы).

Примером схемы нормального алгоритма в пятибуквенном алфавите | * abc может служить схема

Базис логического программирования - student2.ru

Процесс применения нормального алгоритма к произвольному слову V в алфавите этого алгорифма представляет собой дискретную последовательность элементарных шагов, состоящих в следующем. Пусть V' — слово, полученное на предыдущем шаге работы алгорифма (или исходное слово V, если текущий шаг является первым). Если среди формул подстановки нет такой, левая часть которой входила бы в V', то работа алгоритма считается завершённой, и результатом этой работы считается слово V'. Иначе среди формул подстановки, левая часть которых входит в V', выбирается самая верхняя. Если эта формула подстановки имеет вид Базис логического программирования - student2.ru , то из всех возможных представлений слова V' в виде RLS выбирается такое, при котором R — самое короткое, после чего работа алгоритма считается завершённой с результатом RDS. Если же эта формула подстановки имеет вид Базис логического программирования - student2.ru , то из всех возможных представлений слова V' в виде RLS выбирается такое, при котором R — самое короткое, после чего слово RDS считается результатом текущего шага, подлежащим дальнейшей переработке на следующем шаге.

Различные определения алгоритма в явной или неявной форме содержат следующий ряд общих требований:

Дискретность — алгоритм должен представлять процесс решения задачи как последовательное выполнение некоторых простых шагов. При этом для выполнения каждого шага алгоритма требуется конечный отрезок времени, то есть преобразование исходных данных в результат осуществляется во времени дискретно.

Детерминированность — определённость. В каждый момент времени следующий шаг работы однозначно определяется состоянием системы. Таким образом, алгоритм выдаёт один и тот же результат (ответ) для одних и тех же исходных данных. В современной трактовке у разных реализаций одного и того же алгоритма должен быть изоморфный граф. С другой стороны, существуют вероятностные алгоритмы, в которых следующий шаг работы зависит от текущего состояния системы и генерируемого случайного числа. Однако при включении метода генерации случайных чисел в список «исходных данных», вероятностный алгоритм становится подвидом обычного.

Понятность — алгоритм для исполнителя должен включать только те команды, которые ему (исполнителю) доступны, которые входят в его систему команд.

Завершаемость (конечность) — при корректно заданных исходных данных алгоритм должен завершать работу и выдавать результат за конечное число шагов. С другой стороны, вероятностный алгоритм может и никогда не выдать результат, но вероятность этого равна 0.

Массовость — универсальность. Алгоритм должен быть применим к разным наборам исходных данных.

Результативность — завершение алгоритма определёнными результатами.

Алгоритм содержит ошибки, если приводит к получению неправильных результатов либо не даёт результатов вовсе.

Алгоритм не содержит ошибок, если он даёт правильные результаты для любых допустимых исходных данных

Вычислимой называется функция Базис логического программирования - student2.ru от одного или нескольких натуральных аргументов, натуральные значения которой получаются в результате выполнения некоторого алгоритма.

Базис логического программирования

Интерпретировать формулу логики высказываний, значит приписать значения истинности составляющим ее элементарным высказываниям и вычислить истинностное значение всей формулы.

Элементарное высказывание (буква) является формулой нулевого уровня. Если элементарное высказывание всегда верно, мы будем его обозначать буквой И, а если оно всегда неверно, — буквой Л. Тогда формулы первого уровня — это элементарные высказывания, к которым применена только одна логическая связка.

Пусть Ф1 и Ф2 — формулы ненулевого уровня. Тогда записи ((Ф1)), ((Ф1)&(Ф2)), ((Ф1)V(Ф2)), ((Ф1)->(Ф2)), ((Ф1)~(Ф2)) также являются формулами. Если же одна из формул Ф1 и Ф2 , к которым применяется логическая связка, имеет нулевой уровень, то она в скобки не заключается.

Формула — это либо атом, либо одна из следующих конструкций: Базис логического программирования - student2.ru , где F,F1,F2 — формулы, а x — переменная.

Переменная x называется связанной в формуле F, если F имеет вид Базис логического программирования - student2.ru либо Базис логического программирования - student2.ru , или же представима в одной из форм Базис логического программирования - student2.ru , причем x уже связанна в H, F1 и F2. Если x не связанна в F, ее называют свободной в F. Формулу без свободных переменных называют замкнутой формулой, или предложением. Теорией первого порядка называют любое множество предложений.

Логика первого порядка обладает рядом полезных свойств, которые делают ее очень привлекательной в качестве основного инструмента формализации математики. Главными из них являются полнота (это означает, что для любой формулы выводима либо она сама, либо ее отрицание) и непротиворечивость (ни одна формула не может быть выведена одновременно со своим отрицанием). При этом если непротиворечивость более или менее очевидна, то полнота — нетривиальный результат полученный Гёделем в 1930 году (теорема Гёделя о полноте). По сути теорема Гёделя устанавливает фундаментальную эквивалентность понятий доказуемости и общезначимости.

Система логических аксиом логики первого порядка состоит из аксиом исчисления высказываний дополненной двумя новыми аксиомами:

Базис логического программирования - student2.ru ,

Базис логического программирования - student2.ru ,

где A[t / x] — формула, полученная в результате подстановки терма t вместо переменной x в формуле A.

Правил вывода 2:

Modus ponens:

Базис логического программирования - student2.ru

Правило обобщения (GEN):

Базис логического программирования - student2.ru

Под упрощением формулы, не содержащей операций импликации и эквиваленции, понимают равносильное преобразование, приводящее к формуле, которая либо содержит по сравнению с исходной меньшее число операций конъюнкции и дизъюнкции и не содержит отрицаний неэлементарных формул, либо содержит меньшее число вхождений переменных.

Коммутативность: x Базис логического программирования - student2.ru y = y Базис логического программирования - student2.ru x, Базис логического программирования - student2.ru {&, Базис логического программирования - student2.ru }.

Идемпотентность: x Базис логического программирования - student2.ru x = x, Базис логического программирования - student2.ru {&, Базис логического программирования - student2.ru }.

Ассоциативность: (x Базис логического программирования - student2.ru y) Базис логического программирования - student2.ru z = x Базис логического программирования - student2.ru (y Базис логического программирования - student2.ru z), Базис логического программирования - student2.ru {&, Базис логического программирования - student2.ru }.

Дистрибутивность конъюнкций и дизъюнкции относительно дизъюнкции, конъюнкции и суммы по модулю два соответственно:

x Базис логического программирования - student2.ru (y Базис логического программирования - student2.ru z) = (x Базис логического программирования - student2.ru y) Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru z),

x Базис логического программирования - student2.ru (y Базис логического программирования - student2.ru z) = (x Базис логического программирования - student2.ru y) Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru z),

x Базис логического программирования - student2.ru (y Базис логического программирования - student2.ru z) = (x Базис логического программирования - student2.ru y) Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru z).

Законы де Мо́ргана:

Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru y) = ( Базис логического программирования - student2.ru x) Базис логического программирования - student2.ru ( Базис логического программирования - student2.ru y),

Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru y) = ( Базис логического программирования - student2.ru x) Базис логического программирования - student2.ru ( Базис логического программирования - student2.ru y).

Законы поглощения:

x Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru y) = x,

x Базис логического программирования - student2.ru (x Базис логического программирования - student2.ru y) = x.

Другие (1):

x Базис логического программирования - student2.ru ( Базис логического программирования - student2.ru x) = x Базис логического программирования - student2.ru 0 = x Базис логического программирования - student2.ru x = 0.

x Базис логического программирования - student2.ru ( Базис логического программирования - student2.ru x) = x Базис логического программирования - student2.ru 1 = x Базис логического программирования - student2.ru x = x Базис логического программирования - student2.ru x = 1.

x Базис логического программирования - student2.ru x = x Базис логического программирования - student2.ru x = x Базис логического программирования - student2.ru 1 = x Базис логического программирования - student2.ru 0 = x Базис логического программирования - student2.ru 0 = x.

x Базис логического программирования - student2.ru 1 = x Базис логического программирования - student2.ru 0 = x Базис логического программирования - student2.ru 0 = x Базис логического программирования - student2.ru x = x Базис логического программирования - student2.ru x = Базис логического программирования - student2.ru x.

Базис логического программирования - student2.ru .

Другие (2):

Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru .

Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru .

Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru .

Базис логического программирования - student2.ru

Другие (3) (Дополнение законов де Мо́ргана):

Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru .

Базис логического программирования - student2.ru = Базис логического программирования - student2.ru = Базис логического программирования - student2.ru .

Следующая формальная грамматика описывает все формулы, приведенные к КНФ:

<КНФ> → <дизъюнкт>

<КНФ> → <КНФ> ∧ <дизъюнкт>

<дизъюнкт> → <литерал>

<дизъюнкт> → (<дизъюнкт> ∨ <литерал>)

<литерал> → <терм>

<литерал> → <терм>

где <терм> обозначает произвольную булеву переменную.

Исчисление высказываний

Пусть C1 и C2 - два предложения в исчислении высказываний, и пусть Базис логического программирования - student2.ru , а Базис логического программирования - student2.ru , где P - пропозициональная переменная, а C'1 и C'2 - любые предложения (в частности, может быть, пустые или состоящие только из одного литерала).

Правило вывода

Базис логического программирования - student2.ru

называется правилом резолюции.

Предложения C1 и C2 называются резольвируемыми (или родительскими), предложение Базис логического программирования - student2.ru - резольвентой, а формулы P и Базис логического программирования - student2.ru - контрарными литералами.

Исчисление предикатов

Пусть C1 и C2 - два предложения в исчислении предикатов.

Правило вывода

Базис логического программирования - student2.ru

называется правилом резолюции в исчислении предикатов, если в предложениях C1 и C2 существуют унифицированные контрарные литералы P1 и P2, то есть Базис логического программирования - student2.ru , а Базис логического программирования - student2.ru , причём атомарные формулы P1 и P2 являются унифицируемыми наиболее общим унификатором σ.

В этом случае резольвентой предложений C1 и C2 является предложение Базис логического программирования - student2.ru , полученное из предложения Базис логического программирования - student2.ru применением унификатора σ. [2]

Пример: вывод решения в логической модели на основе метода резолюций.

Даны утверждения:

· «Сократ – человек»;

· «Человек – это живое существо»;

· «Все живые существа смертны».

Требуется методом резолюций доказать утверждение «Сократ смертен».

Решение:

Шаг 1.Преобразуем высказывания в дизъюнктивную форму:

Базис логического программирования - student2.ru

Шаг 2. Запишем отрицание целевого выражения (требуемого вывода), т.е. «Сократ бессмертен»:

Базис логического программирования - student2.ru

Шаг 3. Cоставим конъюнкцию всех дизъюнктов (т. е. построим КНФ), включив в нее отрицание целевого выражения:

Базис логического программирования - student2.ru

Шаг 4. В цикле проведем операцию поиска резольвент над каждой парой дизъюнктов:

Базис логического программирования - student2.ru

Получение пустого дизъюнкта означает, что высказывание «Сократ бессмертен» ложно, значит истинно высказывание «Сократ смертен».

Наши рекомендации