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

TL;DR

This paper introduces a recursive, function-based formulation of the Horn algorithm for propositional satisfiability, providing a clear, formal, and inductively provable presentation that enhances understanding and proof simplicity.

Contribution

It offers a novel recursive formulation of the Horn algorithm, enabling concise formalization, step-by-step visualization, and straightforward inductive correctness proofs.

Findings

Formal recursive definition of the Horn algorithm

Simplified inductive correctness proof

Enhanced visualization of algorithm execution

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.