Reduction and Narrowing for Horn Clause Theories
Peter Padawitz · The Computer Journal · 1991
We give an overview of rewrite rule based calculi for reasoning about Horn clause specifications. Such reasoning consists in computing (normal forms), proving (theorems) or solving (goals). Computations are performed by term reduction, proofs are carried out by goal reduction, solutions are obtained by narrowing. The presentation follows our book ‘Computing in Horn Clause Theories’ where we took the viewpoint that most results in this area centre around the soundness or completeness of an inference system. Besides the general calculi of reduction and narrowing we discuss specialisations, which embody particular strategies. For applications to data type specification and program verification, we present the foundations of inductive proof methods based on reduction and narrowing.