| ||||
| ||||
![]() Title:A simple functional presentation and an inductive correctness proof of the Horn algorithm Authors:António Ravara Conference:HCVS 2018 Tags:Correctness proof, Fix-points, horn algorithm, Horn propositional satisfiability algorithm, Inductive Definitions and Recursive functions 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. A simple functional presentation and an inductive correctness proof of the Horn algorithm ![]() A simple functional presentation and an inductive correctness proof of the Horn algorithm | ||||
Copyright © 2002 – 2025 EasyChair |