prolog - 使用归纳法判断给定符号是否在 prolog 中构成有效公式

Question

我们刚刚开始在课堂上学习 prolog，我们的第一个练习如下：

问题：

注意：假设只有两个原子，例如 a 和 b，而不是无限多个。

a) 编写一个prolog 程序，翻译命题逻辑公式的归纳定义（即翻译定义1）。为此，您需要使用：

1.) 一元谓词“at”表示原子公式（因此“at(f)”表示“F 是原子公式”，其中 f 是常数）。

2.) 表示公式的一元谓词“fmla”（因此“fmla(F)”表示“F 是一个公式”）。

3.) 一元运算“neg”表示否定（因此“neg(F)”代表 ¬F）。

4.）二元运算“或”表示两个公式的析取（因此“或（F，G）”代表（F∨G））。

试图：

    at(a). % Our first atom.
    at(b). % Our second atom.

    fmla(F):-
        at(F).

    neg(F):-
        fmla(F).

    or(F,G):-
        fmla(F), fmla(G).

    fmla(F):-
        or(F,G),
        neg(F),
        fmla(G).

有效公式示例：(~A v B) ---> or(neg(a), b)。

我相信我构建程序的方式是正确的，但递归部分不起作用（我在那里也遇到了单例错误）。我试图解决这个问题几个小时但无济于事。任何帮助，将不胜感激。

Answer 1

你已经得到了正确的原子。现在简单地看一下命题逻辑公式的归纳定义：

at(a). % Our first atom.
at(b). % Our second atom.

fmla(F):-           % an atom is a formula
    at(F).

fmla(neg(F)) :-     % neg(F) is a formula if F is a formula
    fmla(F).

fmla(or(F,G)) :-    % or(F,G) is a formula if F and G are formulas
    fmla(F),
    fmla(G).

fmla(and(F,G)) :-   % and(F,G) is a formula if F and G are formulas
    fmla(F),
    fmla(G).

如果您尝试使用上面的示例进行查询：

   ?- fmla(or(neg(a), b)).
yes

是否需要最后一条连接规则取决于您坚持的归纳定义。有些教科书只使用否定和析取，因为连词可以表示为and(A,B) = neg(or(neg(A),neg(B)))。