2018/09/13 by António Ravara
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.278.6
published as EPTCS 278, 2018, pp. 34-48 · In Proceedings HCVS 2018, arXiv:1809.04554
arxiv created 2018/09/13 · arxiv updated 2018/09/14
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.