Prolog语义表展开程序谓词执行顺序与递归机制咨询

该段代码为Prolog语言实现的命题逻辑语义表（Tableau）自动展开工具，接收初始表结构作为输入，递归应用表展开规则后输出完全展开的完成表。

谓词处理顺序的决定机制 #

Prolog的谓词执行没有内置的逻辑算符优先级，处理顺序完全由两点决定：

• 谓词从句的书写顺序：Prolog匹配目标时会严格按照代码中从句的从上到下顺序尝试匹配，只要前面的从句匹配成功，就不会再尝试后面的同谓词从句。这段代码的从句顺序为：双重否定消去规则 > 合取展开规则 > 合取否定的德摩根规则 > 析取展开规则 > 析取否定的德摩根规则 > 字面量处理规则 > 空分支处理规则 > 空输入终止规则，这就是实际运行时的规则优先级。
• 列表的匹配顺序：代码中所有规则都优先匹配当前待处理分支（即列表的第一个子列表）的头部第一个公式，只要分支头部的公式能匹配某条复合公式拆解规则，就会优先拆解该公式，不会先处理分支后面的公式。

递归在展开过程中的作用 #

整个展开流程完全基于递归实现，逻辑对应标准语义表的构造过程：

• 递归终止条件共两个：一是输入待处理分支集合为空expand([],[])，直接返回空结果；二是当前待处理分支为空表expand([[]|T1], [[]|T2])，代表该分支已经没有可拆解的复合公式，标记为完成分支后，继续递归处理剩余的待处理分支集合。
• 递归推进逻辑：每成功匹配一条复合公式展开规则，就按照规则将当前分支头部的复合公式替换为等价形式：双重否定直接消去两层否定保留子公式、合取拆分为两个子公式留在当前分支、析取/合取否定按德摩根律拆分为两个独立分支加入待处理队列，之后对替换后的新表结构递归调用expand继续拆解，直到所有分支都不存在可拆解的复合公式。
• 代码中未标注功能的expand([[X|B]|T1], T5)从句用于处理无法匹配任何复合公式规则的字面量（即单个命题变元或命题变元的否定）：先递归展开当前分支去掉头部字面量X后的剩余部分B，再通过distribute谓词将X添加到B展开后得到的所有子分支头部，之后递归展开其余待处理分支T1，最后将两部分展开结果拼接得到完整表。
• 辅助谓词distribute本身也是递归实现，作用是将指定字面量逐个添加到传入的所有分支的头部，直到分支列表为空时终止。

原实现代码 #

%negation 双重否定消去规则
expand([[not(not(X))|B]|T], T1) :-
    expand([[X|B]|T], T1).

%conjunction 合取相关展开规则
expand([[(X)+(Y)|B]|T], T1):-
    expand([[X, Y|B]|T], T1).

expand([[not((X)+(Y))|B]|T], T1):-
    expand([[not(X)|B], [not(Y)|B]|T], T1).

%disjunction 析取相关展开规则
expand([[(X)/(Y)|B]|T], T1):-
    expand([[X|B], [Y|B]|T], T1).

expand([[not((X)/(Y))|B]|T], T1):-
    expand([[not(X), not(Y)|B]|T], T1).

% 字面量处理与分支收尾逻辑
expand([[X|B]|T1], T5) :-
    expand([B], T2), distribute(X,T2,T3), expand(T1,T4), append(T3,T4,T5).

expand([[]|T1], [[]|T2]) :-
    expand(T1, T2).

expand([],[]).

% 辅助谓词：将字面量X分发到所有分支头部
distribute(X,[B|T],[[X|B]|T1]) :-
        distribute(X,T,T1).

distribute(_,[],[]).

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