Prolog：在 Prolog 中定义逻辑运算符作为其他运算符的占位符

Question

我的目标是在prolog中写一个小证明助手。我的第一步是定义逻辑连接词如下：

:-op(800, fx, -).

:-op(801, xfy, &).

:-op(802, xfy, v).

:-op(803, xfy, ->).

:-op(804, xfy, <->).

:-op(800, xfy, #).

最后一个运算符# 的含义是作为&、v、-> 或<-> 的占位符。我的问题是，我不知道如何在 prolog 中定义它。我尝试通过以下方式解决我的问题：

X # Y :- X v Y; X & Y; X -> Y; X <-> Y.

但以下定义：

proposition(X) :- atomicproposition(X).

proposition(X # Y) :- proposition(X), proposition(Y).

proposition(- X) :- proposition(X). 

与

atomicproposition(a).

给予

?- proposition(a v -a).
false

我做错了什么？

Answer 1

您不能以这种方式定义句法同义词。当你定义类似

X # Y :-
    X & Y.

你定义语义：“执行X # Y，执行X & Y”。但是您还没有定义任何方式来“执行X & Y”：

?- X # Y.
ERROR: Undefined procedure: (&)/2
ERROR: In:
ERROR:    [9] _2406&_2408
ERROR:    [8] _2432#_2434 at /home/isabelle/op.pl:13
ERROR:    [7] <user>

（即使你已经为它定义了一些含义，它也可能不是你想要的。）

您正在寻找的是一种方法来定义不仅“T 是一个带有二元运算符的术语”，而且理想情况下“T 的操作数是 X 和 Y ”。像这样：

binary_x_y(X  v  Y, X, Y).
binary_x_y(X  &  Y, X, Y).
binary_x_y(X  -> Y, X, Y).
binary_x_y(X <-> Y, X, Y).

然后，用：

proposition(X) :-
    atomicproposition(X).
proposition(Binary) :-
    binary_x_y(Binary, X, Y),
    proposition(X),
    proposition(Y).
proposition(- X) :-
    proposition(X).

atomicproposition(a).

我们得到：

?- proposition(a v -a).
true ;
false.

?- proposition(P).
P = a ;
P =  (a v a) ;
P =  (a v a v a) ;
P =  (a v a v a v a) ;
P =  (a v a v a v a v a) ;
P =  (a v a v a v a v a v a) .  % unfair enumeration

还有其他方法可以用更少的输入来表达相同的关系，例如：

binary_x_y(Binary, X, Y) :-
    Binary =.. [Op, X, Y],  % Binary is of the form Op(X, Y)
    member(Op, [v, &, ->, <->]).