我只知道一个证明者可以翻译 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在第二个副本，然后应用以下十个减少规则之一对于每个副本，一次进行尽可能多的规则： …