如何解决Prolog:在Prolog中将逻辑运算符定义为其他运算符的占位符
我的目的是在序言中写一些证明助手。我的第一步是定义逻辑连接词,如下所示:
:-op(800,fx,-).
:-op(801,xfy,&).
:-op(802,v).
:-op(803,->).
:-op(804,<->).
:-op(800,#).
最后一个运算符#的含义是成为&
,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
的操作数是{{1 }}和X
”。像这样:
Y
然后,用:
binary_x_y(X v Y,X,Y).
binary_x_y(X & Y,Y).
binary_x_y(X -> Y,Y).
binary_x_y(X <-> Y,Y).
我们得到:
proposition(X) :-
atomicproposition(X).
proposition(Binary) :-
binary_x_y(Binary,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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。