如果在Prolog中查询无效，SLD树是否存在？

Question

考虑以下Prolog程序：

reverse_bits([1], [0]).
reverse_bits([0], [1]).
reverse_bits([H|T], [0|R]) :- H==1, reverse_bits(T, R).
reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).

上述问题的SLD树是什么？

reverse_bits(Input, [1, 0, 0]).?

这是无效的，所以它甚至还存在一个SLD树吗？

Answer 1

这里是使用sldnfdraw包的最小示例。首先，使用library documentation中指定的语法生成程序并进行查询：

% estamos.pl

:- use_module(library(sldnfdraw)).
:- sldnf.

:- begin_program.

reverse_bits([1], [0]).
reverse_bits([0], [1]).
reverse_bits([H|T], [0|R]) :- H==1, reverse_bits(T, R).
reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).

:- end_program.

:- begin_query.

reverse_bits(Input,[1,0,0]).

:- end_query.

下一步，为相关的分辨率树生成一个.tex文件：

?- draw_goal('estamos-tree.tex').

您可以从命令行运行此目标。最后，将此文件包含在.tex文档中

% estamos-tree-draw.tex

\documentclass{article}
\usepackage{epic,eepic}
\usepackage{ecltree}
\begin{document}
\input{estamos-tree}
\end{document}

并编译为

$ latex estamos-tree-draw.tex
$ dvipdf estamos-tree-draw.dvi

源文件夹中应该有一个包含分辨率树的.pdf文件。

代码改进

关于它的价值，我建议将程序编写为：

reverse_bits([],[]).
reverse_bits([0|T],[1|R]) :- reverse_bits(T,R).
reverse_bits([1|T],[0|R]) :- reverse_bits(T,R).

为简单起见，并避免使用==代替统一，如注释中提到的[[false。

使用=（统一）时的输出

在这里，我们在[防护部分]测试=中使用H统一。

使用==（等效项）时的输出

[使用term equivalence ==时，我们很快就完成了，因为第一次调用失败：

因为匹配的唯一子句是reverse_bits([H|T], [1|R]) :- H==0, reverse_bits(T, R).，并且在这一点上，H是一个新鲜变量，绝不等同于0。