Пролог логики первого порядка
Я пытаюсь найти способ поместить следующее логическое выражение первого порядка в Пролог:
(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)