У меня есть стандартный тип данных, представляющий формулы логики предикатов. Функция, представляющая правило исключения естественного вывода для дизъюнкции, может выглядеть так:
d_el p q =
if p =: (Dis r s) && q =: (Neg r) then Just s else
if q =: (Dis r s) && p =: (Neg r) then Just s else
Nothing where r,s free
x =: y = (x =:= y) == success
Вместо того, чтобы оценивать значение Nothing, когда объединение не удается, функция не возвращает никаких решений в PACKS
:
logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.
Что мне не хватает и почему не el
вычисляет Ничего
при сбое объединения?