Prolog:在 Prolog 中定义逻辑运算符作为其他运算符的占位符
Prolog: define logical operator in Prolog as placeholder for other operator
我的目标是在序言中写一个小证明助手。我的第一步是定义逻辑连接词如下:
:-op(800, fx, -).
:-op(801, xfy, &).
:-op(802, xfy, v).
:-op(803, xfy, ->).
:-op(804, xfy, <->).
:-op(800, xfy, #).
最后一个运算符 # 的含义只是作为 &
、v
、->
或 <->
的占位符。我的问题是,我不知道如何在序言中定义它。我尝试通过以下方式解决我的问题:
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
我做错了什么?
您不能以这种方式定义句法同义词。当你定义类似
的东西时
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, &, ->, <->]).
我的目标是在序言中写一个小证明助手。我的第一步是定义逻辑连接词如下:
:-op(800, fx, -).
:-op(801, xfy, &).
:-op(802, xfy, v).
:-op(803, xfy, ->).
:-op(804, xfy, <->).
:-op(800, xfy, #).
最后一个运算符 # 的含义只是作为 &
、v
、->
或 <->
的占位符。我的问题是,我不知道如何在序言中定义它。我尝试通过以下方式解决我的问题:
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
我做错了什么?
您不能以这种方式定义句法同义词。当你定义类似
的东西时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, &, ->, <->]).