我正在尝试实现一个
unfold
谓词,它采用一个命题公式并返回一个唯一的逻辑运算符是合取、析取和否定的公式。
代码:
:- op(1060, yfx, <->).
:- op(1050, yfx, <-).
:- op(800, yfx, xor).
:- op(600, yfx, v).
:- op(400, yfx, &).
:- op(200, fy, ¬).
define((F xor G), ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)).
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).
% Base case: atomic formula
unfold(A, A) :- atom(A).
unfold(¬ A, NA) :- unfold(A, UA), define(UA, NA1), NA = ¬ NA1.
unfold(A & B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 & C2.
unfold(A v B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 v C2.
unfold(A xor B, C) :- unfold(A, UA), unfold(B, UB), define((UA xor UB), C).
unfold(A <-> B, C) :- unfold(A, UA), unfold(B, UB), define((UA <-> UB), C).
unfold(A <- B, C) :- unfold(A, UA), unfold(B, UB), define((UA <- UB), C).
unfold(A -> B, C) :- unfold(A, UA), unfold(B, UB), define((UA -> UB), C).
然而,那是行不通的。起初我错过了基本情况,然后我添加了它但我只得到
false
。例如,此查询应返回:
-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p).
感谢您的任何指导或帮助。