Построение доказательства разрешения с использованием логики первого порядка

У меня есть следующий обзорный вопрос к предстоящему экзамену, с которым я хотел бы получить некоторую помощь. Я должен ответить на запрос «Мэри использует только зеленые яблоки для приготовления пирогов», используя разрешение. Моя текущая база знаний и язык - это следующие предложения:

Mary only uses apples from John to make pies:
 ∀π,a(Apple(a) ∧ Pie(π) ∧ Make(M,π,a) => Grows(J,a))
(⌐Apple(a) V ⌐Pie(π) V ⌐Make(M, π, a) V Grows(J,a))    (in CNF)

Последнее обновление:

Я постараюсь быть более конкретным в целом. Я хочу доказать, что «Мэри использует только зеленые яблоки для приготовления пирогов». Написав эту логику, я получаю:

Мэри использует только зеленые яблоки для приготовления пирогов: π, Pie (π) A Make (M, π, a) => Green (a)

И шаги по его переводу в форму CNF (http://en.wikipedia.org/wiki/Conjunctive_normal_form):

π,a ⌐(Pie(π) A Make(M, π, a)) V Green(a) 
π,a (⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
(⌐Pie(π) V ⌐Make(M, π, a)) V Green(a) 
⌐Pie(π) V ⌐Make(M, π, a) V Green(a) (CNF form)

Отрицание этого утверждения в форме CNF (которую мы будем использовать в резолюции для доказательства):

Pie (π) A Make (M, π, a) A ⌐Зеленый (a)

Теперь при использовании разрешения для логики первого порядка: (http://en.wikipedia.org/wiki/Resolution_ (логика))

Это правильно!? Или я ошибаюсь?


artificial-intelligence first-order-logic
person user1319951    schedule 09.06.2012    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Я не уверен, что вы подходите к проблеме правильно. Первым шагом является кодирование трех утверждений («Яблоки либо зеленые, либо красные», «Джон выращивает только зеленые яблоки», «Мэри использует яблоки Джона только для приготовления пирогов») в клаузальную форму, чего вы еще не сделали.

Второй шаг - закодировать отрицание утверждения, которое вы пытаетесь доказать («Мэри использует только зеленые яблоки для приготовления пирогов»), также в клаузальную форму. Я не думаю, что вы это сделали, я думаю, вы закодировали положительное утверждение. Возможно, я что-то упускаю. Но кодирование отрицания оператора запроса заканчивается четырьмя короткими операторами, связанными с операторами AND, каждый из которых может рассматриваться как оператор в базе знаний.

Отсюда уменьшение механическое.

Обновление. Еще раз, вам нужно добавить отрицание утверждения, которое вы пытаетесь доказать. Вы этого не делаете, вы добавляете само утверждение и другое утверждение о том, что яблоки зеленые. Не делай этого. Вы не пытаетесь доказать утверждение о том, что яблоки зеленые, вы пытаетесь доказать утверждение о том, что Мэри использует только зеленые яблоки для приготовления пирога. Отвергните это утверждение, разрешите его с помощью трех других операторов базы знаний и извлеките противоречие (то есть разрешите X и не-X вместе для некоторого утверждения X.)

Это алгоритм. Оно работает. Если вы этого не сделаете, независимо от того, «нужно» вам это или нет, вы делаете что-то другое, кроме алгоритма разрешения, и если бы я оценивал ваше домашнее задание / экзамен, я бы оценил его как неправильный.

Обновление 2: вы приближаетесь, но в вашем операторе запроса требуется дополнительное предложение о том, что вы являетесь Apple (например, Apple (a)), как это уже сделано в некоторых других ваших утверждениях. Он должен выглядеть почти точно так же, как утверждение о Мэри, только использующей яблоки Джона (а затем отвергнутым, потому что это запрос). Его форма правильная, с небольшими предложениями, соединенными вместе с AND, вам просто не хватает одного.

Но затем обратите внимание, что, как только вы это сделаете, каждое из этих небольших предложений (потому что они связаны с AND) может действовать как независимое утверждение в вашей базе знаний. Так, например, как вы это сформулировали прямо сейчас, вы можете разрешить Pie (p) с выражением для вашего третьего оператора. В доказательстве разрешения есть много шагов, но как только вы полностью закодируете отрицание запроса, все они будут такими крошечными шагами.

person Novak    schedule 10.06.2012
comment
Спасибо. Теперь я понял, что было не так с моим предыдущим постом. Я обновлю его в ближайшее время - person user1319951; 12.06.2012

arrow_upward
1
arrow_downward

В качестве общей информации вам необходимо иметь свою базу знаний в CNF и ОТРИЦАТЕЛЬНУЮ цель (также в CNF). Затем, унифицируя и применяя разрешение, вам нужно либо иметь нулевую резольвенту, либо само состояние цели. Другой вариант - не найти ничего из этого и разрешить бесконечно.

If 

Make(p,π,a)

находится в вашей базе знаний, затем объедините и примените разрешение с последней резольвентой, которая:

⌐Make(M,π,a)

дает вам нулевую резольвенту. На этом вы можете остановиться и закончить.

person phantasmagoria    schedule 11.06.2012
comment
Вы уверены, что это так просто? Я тоже думал об этом, но я действительно не понимаю, как это напрямую связано с тем, что яблоки зеленые? Или вы предлагаете ввести новое предложение, которое подразумевает Make (p, π, a)? Возможно также справедливо только сказать, что Make (p, f (π), a), где f (π) - это подмножество всех пирогов (при использовании теоремы Сколема для его преобразования). Мне почему-то немного не по себе, просто получая Make (p, π, a) непосредственно из моей базы знаний. Но достаточно ли этого? - person user1319951; 11.06.2012
comment
@ user1319951 Если Make (p, π, a) задано в базе знаний, вам не нужно вводить новое предложение, которое дает импликацию Make (p, π, a). Это уже дано и верно. Вы нашли его отрицательный пункт. Ну это все. На самом деле не нужно над этим сильно задумываться, просто применяйте правила. Это кажется слишком простым, но на самом деле это так. - person phantasmagoria; 12.06.2012
comment
@ user1319951 Между прочим, после того, как у вас есть формы предложений CNF, вы не имеете ничего общего с функцией Сколема. Используется при преобразовании в CNF. Если у вас есть CNF, все, что вы делаете, - это объединяйтесь и решительно в цикле, пока не достигнете своей цели. - person phantasmagoria; 12.06.2012
comment
Что вы думаете о моей новой версии? - person user1319951; 12.06.2012
comment
@ user1319951 Вроде правильно. Однако вы должны четко определить символы (a, a1, a2, π, p, M, J), которые вы используете, являются ли они переменными или константами. Например, если a1 и a2 - константы, второй этап процедуры решения будет неправильным. Я полагаю, что это переменные, вы достигли нулевой резольвенты, так что нет проблем. - person phantasmagoria; 12.06.2012