Justification Based on Program Transformation (Extended Abstract)
Hai-Feng Guo, C. R. Ramakrishnan, I. V. Ramakrishnan · 2003
Justifying the truth value of a goal resulting from query evaluation of a logic program corresponds to providing evidence, in terms of a proof, for this truth. Justification plays a fundamental role in automatic verification, especially model checking [1]. For instance it can be used for efficient generation of parse trees, synthesis controllers for embedded systems [7], etc. In an earlier work, we had given algorithms [8,2] for justification using a tabled logic programming system. The naturalness of using a tabled logic programming system for justification is that the answer tables created during query evaluation also serve as the witnesses supporting the result. Justifying the truth value of a goal resulting from query evaluation of a logic program corresponds to providing concise evidence, in terms of a proof, for this truth. Toward that end we presented algorithms for justifying such logic programs by post-processing the memo tables created during query evaluation. Justification in this postprocessing fashion is “non-intrusive” in the sense that it is completely decoupled from query evaluation process and is done only after the evaluation is completed. Justification is done in a post-evaluation phase, by meta-interpreting the memo tables and clauses of the program. This is a major source of inefficiency because meta-interpretation can be significantly slower than the original query evaluation. Moreover, to avoid cyclic explanations we have to maintain a history of the literals that have been used on the proof path. Prior to adding another literal to the proof we have to check if it already appears in the history, a procedure that suffers from quadratic time complexity. In the full paper [3] we present a general justification technique based on program transformation [5]. First consider justifying true literals. For each literal of the form p(t) the transformation generates a literal pt(t, Y ) such that whenever p(t)θ succeeds for some substitution θ, pt(t, Y )θ succeeds, and in addition, Yθ represents a valid proof for p(t)θ. This extra-argument scheme, however, cannot be directly used for tabled programs. Consider a tabled logic program with cyclically defined clauses. A single answer can have infinite number of valid proof paths, and the transformed program will attempt to capture each of these Research partially supported by NSF awards EIA-9705998, CCR-9876242, IIS0072927, EIA-9901602 and CCR-0205376.