我正在尝试从公式中提取符号。前任：
?- formula((p v q) & (q v r), U).
U = [p, q, v].
到目前为止我所做的：
simbol_formula([],[]).
simbol_formula(negation X, [X]).
simbol_formula(X or Y, [X,Y]).
simbol_formula(X and Y, [X,Y]).
我相信我所做的是正确但不完整的。我被困住了。它显然适用于简单的公式，但不适用于更复杂的公式。我知道我必须将某些东西定义为simbol_formula(F,U) :-. 以某种方式使用递归或将给定的公式分解为“较小”的公式。
您的情况的核心问题是使用默认数据结构。
在您的表示中，您不能仅通过模式匹配来区分：
为了克服这个缺点，我建议用（任意）函子 唯一地标记符号s/1。
例如，公式(p v q) & (q v r)将表示为：
( s (p) ∨ s (q)) & ( s (q) ∨ s (r))
然后，我们可以使用DCG将公式与符号相关联：
符号（s（X））-> [X]。 符号（否定（F））->符号（F）。 符号（X ∨ Y）-> 符号（X），符号（Y）。 符号（X & Y）-> 符号（X），符号（Y）。
示例查询：
?- 短语(符号((s(p) ∨ s(q)) & (s(q) ∨ s(r))), Ls)。 Ls = [p, q, q, r]。
我将定义合适的运算符作为练习，以便上述编译。
以上也可用于枚举公式，尽管不公平：
?- 短语（符号（公式），Ls）。 公式 = s(_G1010), LS = [_G1010] ; 公式=否定（s（_G1012））， LS = [_G1012] ; 公式=否定（否定（s（_G1014）））， Ls = [_G1014] 。