时间戳

首页 > 解决方案 > Prolog：在 Prolog 中定义逻辑运算符作为其他运算符的占位符

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

问题描述

我的目标是在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

我做错了什么？

标签： prologoperator-keywordplaceholder

解决方案

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

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, &, ->, <->]).

推荐阅读