LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation (Q1111776)

Testing for the satisfiability of a Horn expression in propositional calculus is a fundamental problem in the area of logic programming for many reasons. Among these is the fact that the basic solution techniques for propositional Horn formulae have been shown to be central to the design of efficient interpreters for some predicate logic-based languages such as Hornlog [\textit{J. H. Gallier} and \textit{S. Raatz}, J. Logic Program. 4, 119-155 (1987; Zbl 0641.68145)]. The present paper proposes a simplified way of deriving a linear-time algorithm avoiding many of the intricacies of previously known descriptions. In addition, a full, ready- to-use computer code is provided at the end of the paper together with a detailed analysis of the necessary data structures.