Prolog归结求解器递归问题：实现两子句全归结并保留原列表元素

问题描述 #

给定分别存储正负文字、代表子句的两个列表，需要获取这两个子句所有可能的归结结果。
现有初始实现代码如下：

resolution([pos(X)|T],[H2|T2],R):- select(neg(X), [H2|T2],L),union(T,L,R).
resolution([neg(X)|T],[H2|T2],R):- select(pos(X),[H2|T2],L),union(T,L,R).   
resolution([H|T],[H2|T2],R):-resolution(T,[H2|T2],R).

现有代码缺陷 #

上述代码仅能匹配第一个列表的首个文字完成归结，由于递归逻辑问题，每次递归都会丢失列表头部元素，最终得到的是第二个列表和第一个列表删除匹配文字后剩余子集的并集，而非两个原始子句剔除互补对后的并集。
需要遍历第一个列表的所有元素分别和第二个列表做归结，同时保留第一个列表中未参与归结的所有元素。

运行示例 #

现有代码运行结果：

?-resolution([pos(1),neg(3),pos(4)],[neg(1),pos(3),neg(5)],R).
R = [neg(3), pos(4), pos(3), neg(5)] 
R = [pos(4), neg(1), neg(5)]

上述结果分别匹配pos(1)与neg(1)、neg(3)与pos(3)完成归结，但是第二个结果丢失了第一个子句中未参与归结的pos(1)元素。
期望输出结果如下：

?-resolution([pos(1),neg(3),pos(4)],[neg(1),pos(3),neg(5)],R).

R = [neg(3), pos(4), pos(3), neg(5)]
R = [pos(1),pos(4), neg(1), neg(5)]

解决方案 #

问题核心是原始实现递归遍历时直接丢弃了未匹配的头部元素，我们可以通过select/3内置谓词完成子句元素遍历，自动保留未参与归结的所有元素：

% 主归结谓词
resolution(Clause1, Clause2, Resolvent) :-
    % 从第一个子句中任选一个文字，同时得到剩余文字集合
    select(Literal, Clause1, RestClause1),
    % 获取该文字的互补文字
    complementary(Literal, ComplementLiteral),
    % 从第二个子句中选中该互补文字，同时得到剩余文字集合
    select(ComplementLiteral, Clause2, RestClause2),
    % 两个剩余集合取并集得到归结结果
    union(RestClause1, RestClause2, Resolvent).

% 定义正负文字的互补规则
complementary(pos(X), neg(X)).
complementary(neg(X), pos(X)).

实现说明 #

• select/3会自动遍历目标列表的所有元素，同时返回移除选中元素后的完整剩余列表，不需要手动写递归遍历逻辑，避免了头部元素丢失的问题
• 单独抽离complementary/2谓词定义互补规则，代码可维护性更高
• 运行目标查询即可完全匹配期望的输出结果

内容的提问来源于stack exchange，提问作者krs