Пролог - формулы в логике высказываний - PullRequest
Новая
       8

Пролог - формулы в логике высказываний

5 голосов
/ 16 октября 2010

Я пытаюсь создать предикат, чтобы проверить, соответствует ли заданный вход формуле.

Мне разрешено использовать только для пропозициональных атомов, таких как p, q, r, s, t и т. Д. Формулы, которые я должен проверить, следующие: 

neg(X) - represents the negation of X  
and(X, Y) - represents X and Y  
or(X, Y) - represents X or Y  
imp(X, Y) - represents X implies Y

Я сделал предикат wff, который возвращает true, если заданная структура является формулой, и false в противном случае. Кроме того, мне не нужно использовать переменные внутри формулы, только пропозициональные атомы, как упомянуто ниже. 

logical_atom( A ) :-
    atom( A ),     
    atom_codes( A, [AH|_] ),
    AH >= 97,
    AH =< 122.

wff(A):-
    \+ ground(A),
    !,
    fail.

wff(and(A, B)):-
    wff(A),
    wff(B).

wff(neg(A)):-
    wff(A).

wff(or(A, B)):-
    wff(A),
    wff(B).

wff(imp(A, B)):-
    wff(A),
    wff(B).

wff(A):-
    ground(A),
    logical_atom(A),
    !.

Когда я ввожу такой тест, wff(and(q, imp(or(p, q), neg(p))))., вызов возвращает значения true и false. Подскажите, пожалуйста, почему так происходит?

1 Ответ

10 голосов
/ 16 октября 2010

Структура данных, которую вы выбрали для представления формул, называется «дефолтной», поскольку для проверки атомарных идентификаторов необходим регистр «по умолчанию»: все, что является , а не чем-то из перечисленного выше (и, или,neg, imp) и удовлетворяет логическому_атому / 1 является логическим атомом (в вашем представлении).Интерпретатор не может различить эти случаи по их функтору для применения индексации первого аргумента.Гораздо чище, по аналогии и / или / и т. Д., Также снабдить атомарные переменные их выделенным функтором, скажем, «atom (...)».wff / 1 может затем прочитать: 

wff(atom(_)).
wff(and(A, B))    :- wff(A), wff(B).
wff(neg(A))       :- wff(A).
wff(or(A, B))     :- wff(A), wff(B).
wff(imp(A, B))    :- wff(A), wff(B).

Ваш запрос теперь детерминирован по желанию: 

?- wff(and(atom(q), imp(or(atom(p), atom(q)), neg(atom(p))))).
true.

Если ваши формулы изначально не представлены таким образом, лучше сначалапреобразовать их в такую ​​форму, а затем использовать такое представление, которое не является неплатежеспособным для дальнейшей обработки.

Дополнительным преимуществом является то, что теперь вы можете легко не только проверять, но и перечислять хорошоформул с кодом типа: 

wff(atom(_))  --> [].
wff(and(A,B)) --> [_,_], wff(A), wff(B).
wff(neg(A))   --> [_], wff(A).
wff(or(A,B))  --> [_,_], wff(A), wff(B).
wff(imp(A,B)) --> [_,_], wff(A), wff(B).

и запросом типа: 

?- length(Ls, _), phrase(wff(W), Ls), writeln(W), false.

Выход: 

atom(_G490)
neg(atom(_G495))
and(atom(_G499),atom(_G501))
neg(neg(atom(_G500)))
or(atom(_G499),atom(_G501))
imp(atom(_G499),atom(_G501))
and(atom(_G502),neg(atom(_G506)))
and(neg(atom(_G504)),atom(_G506))
neg(and(atom(_G504),atom(_G506)))
neg(neg(neg(atom(_G505))))
neg(or(atom(_G504),atom(_G506)))
neg(imp(atom(_G504),atom(_G506)))
etc.

в качестве вывода.

...