логика первого порядка пролога

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

(p(0) or p(1)) and not (p(0) and p(1))

Это означает, что он должен отвечать на запросы следующим образом:

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No.

Я попытался перевести логическое выражение:

(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1)

Используя автодополнение Кларка (которое гласит, что любая дефиниционная теория может быть помещена в логическую программу, указав if-половинки), я могу получить:

p(0) :- not p(1).

К сожалению, полученная в результате теория является только здравой (из нее не будет получена ложная информация), но не полной (например: p (1) не может быть выведен). Это следствие теоремы Кларка.

Кто-нибудь знает, есть ли лучшее решение? Спасибо!


logic prolog theorem
person marczoid    schedule 28.09.2012    source источник
comment
Какая семантика у вашего языка? Нет ли противоречия? доказуемо? Когда вы говорите p(0), вы спрашиваете об этом у системы или сообщаете системе? Считается ли, что все, что не указано, ложно (как в закрытом мире Пролога), или может принимать какое-либо значение?   -  person Will Ness    schedule 29.09.2012
comment
Я использую семантику Завершение Кларка. Логическое значение запросов: доказуемо, поэтому ?- p(0) эквивалентно вопросу, можно ли p(0) доказать с помощью теории.   -  person marczoid    schedule 07.11.2012

Ответы (4)


arrow_upward
3
arrow_downward

Это незаметно, но на самом деле вы ошибаетесь. Вы не должны ожидать, что влечет за собой p (0). Следование потребовало бы, чтобы p (0) истинно во всех моделях теории. Но у этой теории есть две модели {p (1)} и {p (0)}.

Это широко изучено в литературе. Как вы правильно заметили, завершение Кларка не справляется с этими случаями. Что еще хуже, SLDNF попадает в бесконечную рекурсию для

p(0) :- not p(1). 
p(1) :- not p(0).

Какой перевод является наиболее подходящим для определенных положений вашей теории.

Я избавлю вас от указателей на определение различной семантики, но если вам нужно быстрое и практичное решение, я предлагаю переключиться на Программирование набора ответов.

Вот ссылка на мой любимый решатель (руководство тоже красивое и самодостаточное): http://www.cs.uni-potsdam.de/clasp/

Наслаждаться!

person NotAUser    schedule 01.10.2012
comment
Спасибо! Но я не думаю, что я ошибаюсь, в чем именно ты думаешь, что я не прав? Я действительно решил перейти на ASP неделю назад, это здорово! - person marczoid; 02.10.2012
comment
Я имел в виду ожидание того, что p (1) и p (0) являются следствиями вашей теории. Это верно только при смелой семантике в отличие от скептической естественной семантики Пролога. - person NotAUser; 04.10.2012
comment
Спасибо, думаю, теперь я это понимаю. p (0) и p (1) не являются следствиями моей теории, потому что они не верны во всех моделях (скептически). Напротив, они верны только в некоторых моделях (смелых). - person marczoid; 05.10.2012

arrow_upward
4
arrow_downward

В Прологе, если и p(0), и p(1) завершились успешно, то p(0),p(1) не может потерпеть неудачу.

Это означает, что вам придется создать своего собственного маленького интерпретатора, разработать способы представления ваших целей и правил для него и задавать в нем свои вопросы, например

?- is_true( (p(0),p(1)) ).
person Will Ness    schedule 28.09.2012
comment
Я понимаю, о чем вы говорите, но почему это так? - person marczoid; 07.11.2012
comment
Я имел в виду это как запрос в гипотетическом оценщике / предикате is_true, который реализует вашу семантику. Он ответил бы либо, например, Yes или No. Я думаю, что другие ответили на ваш вопрос здесь более конкретно; попробуйте спросить и их (поставьте комментарий под ответом, чтобы его получил автор ответа). :) - person Will Ness; 07.11.2012

arrow_upward
2
arrow_downward

Логически, уже в логике высказываний, из этого не следует (A v B) | - A и ни (A v B) | - B. Ситуация также не изменится, если вы добавите ~ (A & B).

Вопрос теперь в том, может ли завершение clark или что-то еще добавить дополнительную информацию по умолчанию, чтобы мы, наконец, получили T | - A и T | - B. Но по логике тогда у нас были бы T | - A&B.

Так что я думаю, что в обычных условиях невозможно делать то, что вы хотели бы делать.

Пока

P.S .: Ненормальной обстановкой может быть, например, использование доверчивого отношения последствий вместо скептического отношения последствий. Отношение скептических последствий:

T |- A iff forall M (if M |- T then M |- A)

Легковерное отношение последствий:

T |~ A iff exists M (M |- T and M |- A)

Возможно иметь T | ~ A и T | ~ B, но не T | ~ A&B, ваши (A v B) & ~ (A & B) без какой-либо информации по умолчанию уже является такой теорией.

P.S.S .: Есть несколько способов злоупотребить системой Prolog для легковерных рассуждений, хотя фонд Prologs является скептическим рассуждением. Уловка состоит в том, чтобы использовать тождество T | ~ A = ~ (T | - ~ A).

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

(A v B -> C) == (A -> C) & (B -> C)
person Mostowski Collapse    schedule 29.09.2012
comment
Единственный смысл, который я мог бы понять, это то, если мы интерпретируем ответы, данные OP, как не противоречащие или согласованные. Итак, утверждение A согласуется со знанием K, что (A v B) ^ ~(A ^ B), и поэтому заявляет B, но не заявляет оба A ^ B. Но семантика Пролога подразумевается или, что доказуемо, не является непротиворечивой. - person Will Ness; 29.09.2012
comment
Вовлеченность и последовательность взаимосвязаны. T | - A эквивалентно T, ~ A несовместно. Но вы правы, в ненормальной обстановке мы могли бы иметь T | - A и T | - B, но не T | - A&B. См. Новую правку. - person Mostowski Collapse; 30.09.2012

arrow_upward
2
arrow_downward

Если введение именованного термина разрешено в вашей «целевой» логике, вы можете реализовать фиктивный t / 0:

t :- p(0), p(1), !, fail.
t :- p(0).
t :- p(1).

тогда, если у нас есть оба

p(0).
p(1).

t / 0 выйдет из строя.

person CapelliC    schedule 28.09.2012