Horn算法的一个简单函数表示和一个归纳正确性证明
A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm
摘要：
我们提出了一个递归公式的霍恩算法来决定命题子句的可满足性。命令式伪代码中的通常表示是非正式的，不适合对其主要性质进行简单证明。通过将算法定义为递归函数（计算最小不动点），我们实现了：1）简洁而严格的形式化; 2）可视化算法执行的清晰形式，一步一步; 3）精确的结果，简单的状态和干净的归纳证明。
英文摘要：
We present a recursive formulation of the Horn algorithm for deciding the satisfiability of propositional clauses. The usual presentations in imperative pseudo-code are informal and not suitable for simple proofs of its main properties. By defining the algorithm as a recursive function (computing a least fixed-point), we achieve: 1) a concise, yet rigorous, formalisation; 2) a clear form of visualising executions of the algorithm, step-by-step; 3) precise results, simple to state and with clean inductive proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
