Как показать, что предложение выводится из набора предложений в Prolog?

Question

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

C = m(P,X) <- m(Q,X), m(R,X) 

можно разрешить головку C с первым корпусом буквального С», чтобы дать замену {P/Q',X/X'} и условие:

D = m(P',X') <- m(Q,X'), m(R,X'), m(R',X'). 

Как я могу показать это с помощью Prolog? Другими словами, как я могу показать, что вы можете получить D от C?

Answer 1

Вы уточнили свой вопрос после моего первого сообщения, но под ним уже есть обсуждение. Чтобы избежать путаницы, я не буду редактировать его, но написать второй один:

Есть две причины, почему вы не можете непосредственно запишите вашу проблему как пролог программы:

• вы хотите разрешить без запроса
• вы хотите увидеть резольвенту (одного) вывода этапе

Поэтому мы закодировать базу данных в операторе предиката mi_clause, который имеет два аргумента: голова и список с телом. Предикат clause_clause_resolvent имеет 6 аргументов: head и body для каждого предложения, а также для резольвенты. Здесь резольвента является результатом разрешения над главой второго предложения с первым элементом тела первого предложения. Выполнение этого также будет работать.

mi_clause(m(_P,X), [m(_Q,X), m(_R,X)]). % your original clause, anonymous variables are prefixed with _ for compiler reasons 

clause_clause_resolvent(Head1, Body1, Head2, Body2, RHead, RBody) :- 
    copy_term(clause(Head1,Body1), clause(H1,B1)), % create a variant of the first clause 
    copy_term(clause(Head2,Body2), clause(H2,B2)), % same for second clause 
    B1 = [H2|Rest1],        % the prolog execution order always uses the first literal 
    H1 = RHead,         % head of resolvent is the same (is only resolved with the query) 
    append(Rest1, B2, RBody).      % create the new body 

Комментарии должны быть более или менее понятны: В copy_terms создать варианты пункта ввода, в противном случае вы можете потерять резольвенты. Затем вы выбираете первый элемент тела второй статьи и пытаетесь унифицировать. На самом деле, этого объединения достаточно, чтобы правильно создать оба предложения. Теперь мы создаем наше предложение резольвент: глава пункта 1 переносится (по модулю подстановкой унификатора), тело резольвент - это тело 1-го пункта без разрешенного литерала, добавленного к телу тела второго предложения.

Теперь попробуйте предикат, например, в SWI Prolog:

?- mi_clause(H1,B1), mi_clause(H2,B2), clause_clause_resolvent(H1,B1,H2,B2,RH,RB). 
H1 = m(_G1028, _G1029), 
B1 = [m(_G1034, _G1029), m(_G1040, _G1029)], 
H2 = m(_G1043, _G1044), 
B2 = [m(_G1049, _G1044), m(_G1055, _G1044)], 
RH = m(_G1068, _G1069), 
RB = [m(_G1080, _G1069), m(_G1099, _G1069), m(_G1105, _G1069)]. 

Как вы можете видеть, H1 и H2 варианты вашего п головы, содержащие свежие переменные anonoymous. Тем не менее все элементы RB имеют вид m (_, _G1069), получая вариант предложения, который вы ожидали.

Если вы хотите, чтобы проверить общий шаг разрешения, замените строки B1 = [H2 | Rest1] с member_of_rest (H2, B1, Rest1) и определить это как:

member_of_rest(X, [X|Xs], Xs). 
member_of_rest(X, [H|Xs], [H|Ys]) :- 
    member_of_rest(X, Xs, Ys). 

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

Удачи!

Answer 2

В отличие от общего разрешения Prolog имеет порядок, в котором условия разрешаются. Это означает, что в целом вы не можете заставить пролог разрешить два литерала друг против друга. Основная идея рассуждений в Prolog заключается в том, что в случае предложений Хорна (только один положительный литерал, отрицательные литералы 0+) после каждого шага разрешения вы получаете новое предложение Хорна. Вы можете только подтвердить доказательство пустой статьи, разрешив ее с помощью чисто отрицательного предложения. В Prolog это предложение предоставляется пользователем в форме запроса. Этот запрос ведет к доказательной стратегии Prolog.

Возможно, давайте посмотрим на классический Аристотеле является человеческим примером:

Мы знаем Aristoteles философ (1) и что все философы человек (2). Поэтому Аристотель - человек.

philosopher(aristoteles). % (1) 
human(X) :- philosopher(X). % (2) 

Теперь сформулируем наш запрос:

?- human(aristoteles). % (3) 

Пролог ищет пункта с головкой (положительный) п unifiable с (3) сверху вниз. Глава пункта (1) не объединяется, поэтому мы попробуем предложение (2) и найдем (наиболее общий) унификатор: X = aristoteles. Выведем теперь условие:

:- philosopher(aristoteles). % (4) 

, которые мы можем решить с пунктом (1), опять-таки с объединителем X = Аристотелю. Достигнув пустой оговорки - Ура, у нас есть доказательство!

В этом деривате имеет значение запрос. В вашем случае мы можем сформулировать запрос, который будет делать то, что вы хотели. C1 и C2 то же самое положение (по модулю переименования переменных), поэтому мы записать:

m(P,X) :- m(Q,X), m(R,X). % (5) 

, если мы теперь запросить M (A, Y), мы начинаем процесс выведения, который имитирует шаг, который вы хотели. Разрешающая запрос с (5), может заменить P = A, X = Y и получим:

:- m(Q,A), m(R,A). % (6) 

Мы начинаем пытается решить по т (Q, А), что опять-таки соответствует правилу (5) с Р = Q, а = Х:

:- m(Q,A), m(R,A). % (7) 

Так как положения (6) и (7) являются такими же, то ясно, что ни число шагов разрешения не достигнет пустой пункт. Другими словами, Prolog будет зацикливаться на бесконечном цикле (в зависимости от оптимизации он может даже не заполнить исполняемый стек и не зацикливаться, иначе вы получите ошибку из стека).

Чтобы сделать запрос прекратить, можно добавить тот факт,

m(a,b). % (8) 

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

Надеюсь, это поможет немного понять, что происходит. Если нет, я всегда могу добавить больше;)

P.S. Я сделал небольшой дидактический прыжок - запрос - это отрицание чисто отрицательной оговорки, которую вы должны предоставить теоретическому доказательству. Поскольку запрос определяется пользователем, вы просто думаете, что Prolog выводит его вместо того, чтобы разрешать его отрицанием. Это также помогает вам вводить символы skolem.