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

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

(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) 

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

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

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

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

4 ответа

Решение

Это тонко, но вы на самом деле не правы. Вы не должны ожидать, что 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/

Наслаждайтесь!

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

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

?- is_true( (p(0),p(1)) ).

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

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

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

p(0).
p(1).

T / 0 не удастся.

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

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

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

до свидания

PS: Ненормальным параметром может быть, например, использование доверительных отношений последствий вместо скептических отношений последствий. Соотношение скептических последствий:

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) без какой-либо информации по умолчанию уже являются такой теорией.

PSS: Есть несколько способов злоупотребить системой Prolog для достоверных рассуждений, хотя основание Prolog s - скептическое рассуждение. Хитрость заключается в том, чтобы использовать тождество T |~ A = ~(T |- ~A).

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

(A v B -> C) == (A -> C) & (B -> C)
Другие вопросы по тегам