A Simple Functional Presentation and an Inductive Correctness Proof of the Horn Algorithm

António Ravara
(NOVA LINCS and Dep of Informatics, FCT, NOVA University of Lisbon)

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.

In Temesghen Kahsai and German Vidal: Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2018), Oxford, UK, 13th July 2018, Electronic Proceedings in Theoretical Computer Science 278, pp. 34–48.
Published: 12th September 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.278.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org