Justifying Proofs Using Memo Tables

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


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 determine 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 adding computation overhead to the the existence check.

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 evidence, using the XMC model checker as a test case, which shows the effectiveness of the justifier in practice. Finally we discuss the role of the justifier as a powerful programming abstraction for encoding efficient algorithms as tabled logic programs.

Bibtex Entry:

author = {Abhik Roychoudhury and  C. R. Ramakrishnan and  I. V. Ramakrishnan},
title = {Justifying Proofs Using Memo Tables},
booktitle = {Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming ({PPDP})},
address = {Montreal, Canada},
month = {September},
publisher = {ACM Press},
pages = {178--189},
year = {2000}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan