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.