Justifying Proofs using Memo Tables

Abhik Roychoudhury, C.R. Ramakrishnan and I.V. Ramakrishnan

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

Abstract

Tableau-based proof systems can be elegantly specified and directly executed by a tabled Logic Programming (LP) system. Our experience with the XMC model checker shows that such an encoding can be used to search for the existence of a proof very efficiently. However, the users of a tableau system are often interested in getting sufficient evidence (in terms of the tableau proof rules) on why a proof does or does not exist. In this paper, we address the problem of constructing such an evidence without introducing any additional computational overhead to the proof search.

A tabled LP system maintains a memo table of ``lemmas'' that were tried and possibly proved during query evaluation. We propose the concept of justifier for extracting sufficient evidence for the truth or falsehood of literals in a logic program, by post-processing the memo tables created during query evaluation. We give an efficient algorithm to implement such a justifier. Based on this justifier for logic programs, we show how to construct evidence for the presence or absence of tableaus in a tableau-based proof system. We provide experimental results, using the XMC model checker as a test case, which shows the effectiveness of the justifier in constructing succinct evidence in practice. Finally we discuss the role of the justifier as a powerful programming abstraction for encoding efficient algorithms as tabled logic programs.