пролог поймать все предложения, которые активны, только если нет других предложений

Question

У меня есть предикат, который связывает формальную логическую формулу с ее отрицательной нормальной формой.Все связки, кроме модальных операторов, конъюнкции и дизъюнкции, исключаются, а отрицание проталкивается как можно дальше в листья выражения.

Предикат rewrite/2 has имеет всеобъемлющее предложение rewrite(A, A).это текстуально последний .С помощью этого доступного предложения можно извлечь формулу в отрицательной нормальной форме.В этом примере e является двунаправленным соединительным элементом, как в нотации Лукасевича, а 4 и 7 являются переменными в модальной логике (и, следовательно, константами Пролога).

Z, объединенными с формулойв отрицательной нормальной форме.

?- rewrite(e(4, 7), Z).
Z = a(k(4, 7), k(n(4), n(7)))

Однако rewrite(<some constant>, <some constant>) всегда успешен, и я бы хотел, чтобы он не удался.Предложение catch-all действительно должно быть всеобъемлющим, а не тем, которое потенциально может сработать, если применимо другое предложение.

?- rewrite(e(4, 7), e(4, 7)).
true.

Я попытался заменить rewrite(A, A). на защищенную версию:

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

rewrite(A, A) :- \+ wff_shallowly(A).

Я подумал, что это предотвратит применение универсального предложения тогда и только тогда, когда A не будет возглавляться атомом / конструктором со специальным значением.Однако после внесения этого изменения rewrite всегда завершается ошибкой, если вызывается рекурсивно.

?- rewrite(4, Z).
Z = 4.

?- rewrite(c(4, 7), Z).
false.

Как правильно настроить предложение catch all.

✱ полный текст программы дляссылка:

% so the primitive connectives are
% l <-- necessity
% m <-- possibility
% c <-- implication
% f <-- falsehood
% t <-- truth
% k <-- conjunction
% a <-- alternative
% n <-- negation
% e <-- biconditional

wff_shallowly(WFF) :-
  WFF = l(_);
  WFF = m(_);
  WFF = c(_, _);
  WFF = f;
  WFF = t;
  WFF = k(_, _);
  WFF = a(_, _);
  WFF = n(_);
  WFF = e(_, _).

% falsehood is primitive
rewrite(f, f).

% truth is primitive
rewrite(t, t).

% positive connectives
rewrite(a(A, B), a(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(k(A, B), k(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(l(A), l(C)) :- rewrite(A, C).
rewrite(m(A), m(C)) :- rewrite(A, C).

% implication
rewrite(c(A, B), a(NC, D)) :-
  rewrite(n(A), NC), rewrite(B, D).

% biconditional
rewrite(e(A, B), a(k(C, D), k(NC, ND))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated falsehood is truth
rewrite(n(f), t).

% negated truth is falsehood
rewrite(n(t), f).

% double negation elimination
rewrite(n(n(A)), C) :- rewrite(A, C).

% negated alternation
rewrite(n(a(A, B)), k(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated conjunction
rewrite(n(k(A, B)), a(NC, ND)) :-
  rewrite(n(A), NC), rewrite(n(B), ND).

% negated biconditional
rewrite(n(e(A, B)), a(k(C, ND), k(NC, D))) :-
  rewrite(A, C),
  rewrite(n(A), NC),
  rewrite(B, D),
  rewrite(n(B), ND).

% negated necessity
rewrite(n(l(A)), m(NC)) :- rewrite(n(A), NC).

% negated possibility
rewrite(n(m(A)), l(NC)) :- rewrite(n(A), NC).

% catch all, rewrite to self
rewrite(A, A) :- \+ wff_shallowly(A).

Answer 1

Все эти проблемы исчезают, если вы используете чистое представление ваших данных.

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

Например, давайте использовать функтор v/1 для представления переменных.Это означает, что мы используем v(1), v(7) и т. Д. Для представления модальных переменных 1, 7 и т. Д.

Вместо вашего предложения «catch all» я добавляю следующие пункты, в которых говорится, что относится к модальнымпеременные:

% (negated) variable

rewrite(n(v(V)), n(v(V))).
rewrite(v(V), v(V)).

Теперь мы получаем:

<b>?- rewrite(e(v(4), v(7)), Z).</b>
Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7)))).

Обратите внимание, что мы, конечно, должны использовать оболочку v/1 в запросах, а также получать оболочку в ответах.Это немного сложнее для чтения и записи, чем если бы обертки не было.Однако это упрощает рассуждения о таких формулах, и поэтому я настоятельно рекомендую использовать их.

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

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