我只知道一个证明者可以翻译 Quine 在他的《逻辑方法》一书中为经典命题逻辑给出的算法（Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40），这个证明者是在 Haskell 和它在这里： Haskell 中的 Quine 算法
我试图在Prolog中翻译Quine的算法，但直到现在我还没有成功。很遗憾，因为它是一种高效的算法，而且 Prolog 翻译会很有趣。我将描述这个算法。我在开始时给出的唯一 Prolog 代码是对测试证明者有用的运算符列表：
% operator definitions (TPTP syntax)
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
真值常量分别为top和bot，分别为true和false。该算法开始如下：对于任何命题公式˚F，使这两个副本和替换，其具有最高发生的原子˚F通过top在所述第一拷贝，并通过bot在第二个副本，然后应用以下十个减少规则之一对于每个副本，一次进行尽可能多的规则： …
我正在尝试为 R 中的逻辑变量创建一个“隐含”运算符，以使命题演算更容易。但是，它似乎与否定运算符一起玩得并不好。正如此处的最后 4 行所示，我必须将取反变量括在括号中才能使蕴涵运算符正常工作。
我怀疑运算符优先级是问题，但我不确定。从我读到的内容来看，没有办法改变中缀运算符的优先级。有没有一种方法可以重新定义，implies()以便(!q) %->% (!p)不需要括号？
> implies <- function(p, q) !p | q
> "%->%" <- implies
>
> p <- c(TRUE, TRUE, FALSE, FALSE)
> q <- c(TRUE, FALSE, TRUE, FALSE)
> p %->% q
[1] TRUE FALSE TRUE TRUE
> !q %->% !p
[1] TRUE FALSE FALSE FALSE
> (!q) %->% !p
[1] TRUE FALSE TRUE TRUE
我是 Prolog 新手，有一些疑问。
我需要编写一个函数 form_equiv(A,B) 来告诉我们 B 是否等于 A，其中 A 和 B 应该是命题。
我知道两个命题是等价的，如果
同义反复 (A 当且仅当 B) = TRUE
但是我怎样才能创建一个函数来检查公式何时是同义反复。
顺便说一句，我不能仅使用内置函数 AND、OR 和 NOT。
现在这是我到目前为止所拥有的：
and(P,Q) :- P, Q, !.
or(P,Q) :- (P; Q), !.
impl(P,Q) :- or(not(P),Q).
syss(P,Q) :- and(impl(P,Q),impl(Q,P)).
t.
f :- fail.
t(_).
f(_) :- fail.
:- op(400,xf,not).
:- op(500,xfx,and).
:- op(500,xfx,or).
:- op(600,xfx,impl).
:- op(700,xfx,syss).
我在 Haskell 中完成了一个类似的程序，但我对 Prolog 真的很陌生。
谁能帮我写一个函数来检查公式是否是同义反复？
提前致谢...