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 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:
@inproceedings{RRR:PPDP00, 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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)