The Algebra of Searching

Michael Spivey and Silvija Seres

What is the logic of Prolog? The usual answer is that it is Horn-clause logic, but this answer does justice only to the `declarative' reading of programs, and ignores the implicit control information that is contained in a `procedural' reading. Whilst we may regard two logical specifications as equivalent if they have the same meaning in Horn-clause logic, it is certainly true that logically equivalent programs can have very different operational behaviours. In this paper, we seek to develop a logic for logic programs that takes into account this procedural aspect of their behaviour under different search strategies, emphasizing algebraic properties that are common to all search strategies.