至多一个正文字的含义
¬p∨¬q∨r只有r一个正文字，可改写为(p∧q)→r；其含义是在p和q都成立时必须有r。只含一个正文字的这种规则称为确定子句。单位事实r相当于没有实质前提就要求r成立。
全为负文字的¬p∨¬q也属于霍恩子句，可写成(p∧q)→假，禁止p和q同时为真。因此，“至多一个”不能误写为“恰好一个”，也不能把出现否定文字误当作不是霍恩形式。
参考：[1]
从假开始，只增加被迫为真的变量
对有限命题霍恩公式，可以先把所有变量设为假，再找尚未满足的蕴涵。若其前提已真而结论变量仍假，就把结论设真；若结论是“假”，便发现不可满足。例如事实p与规则p→q会推出q，再有q→假就产生冲突。
每个变量只会从假变成真，至多变化一次，因此这个过程会终止。关键不变量是当前赋值不大于任何满足赋值：只增加所有可能模型都已被规则迫出的真值。没有冲突而达到全部规则成立时，所得是按逐变量真假排序的最小模型。
参考：[1]
命题算法与逻辑编程的边界
逐次扫描规则的简单实现已有多项式时间界限；优化实现还可以记录规则的未满足前提和变量出现位置，减少重复检查。效率依赖霍恩结构，不是任意CNF都能从全假赋值单向推进到答案。
Prolog、Datalog等语言利用一阶霍恩规则表达带参数的关系，执行还涉及变量替换和搜索。一阶项、函数符号及具体求值策略改变问题范围，不能仅见到规则形式就断言整个程序总会终止，或把命题最小模型算法直接视为任意逻辑程序的完整执行器。