A simple functional presentation and an inductive correctness proof of the horn algorithm

Research output: Contribution to journalConference article

Abstract

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.

Original languageEnglish
Pages (from-to)34-48
Number of pages15
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume278
DOIs
Publication statusPublished - 12 Sep 2018
Event5th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2018 - Oxford, United Kingdom
Duration: 13 Jul 2018 → …

Fingerprint Dive into the research topics of 'A simple functional presentation and an inductive correctness proof of the horn algorithm'. Together they form a unique fingerprint.

Cite this