Tabulation-based Induction Proofs with Application to Automated Verification.
Abhik Roychoudhury, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka · 1998
XSB [14] is a tabled logic programming system designed to address shortcomings in Prolog's SLD evaluation mechanism for Horn programs. SLD's poor termination and complexity properties have rendered Prolog unsuitable for deductive database (DDB) and non-monotonic reasoning (NMR) applications. In contrast, XSB's implementation achieves a computationally tight integration of the logic programming (LP), DDB, and NMR paradigms. When tabled resolution is used in XSB (by declaring particular predicates to be tabled), the system automatically maintains a table of predicate invocations and answers, using the table for all equivalent invocations after the first one. Many programs that would loop infinitely in Prolog will terminate in XSB because XSB calls a tabled predicate with the same arguments only once, whereas Prolog may call such a predicate infinitely often. For these terminating programs XSB efficiently computes the least model, which is the least f...