Use of Correctness Assertions in Declarative Diagnosis of Logic Programs

. We use assertions to reduce the quantity of queries in declarative diagnosis of logic programs. We first present a declarative diagnoser for normal logic programs. Given a bug symptom, the diagnoser first constructs a tree that models the execution of the bug symptom and then searches the tree for the bug that causes the bug symptom. We then incorporate into the diagnoser three tree transformations that prune the tree before it is searched. These transformations make use of two kinds of assertion about the correctness of the program and maintain the soundness and completeness of the diagnoser. These transformations reduce the size of the tree and thus reduce the quantity of queries imposed on the oracle. Keywords: Declarative diagnosis; Correctness assertions; Logic programs; Tree transformations 1 Introduction Declarative program diagnosis is an interactive process where a declarative diagnoser obtains the intended interpretation of the program from an oracle, usually the programm..