Loading...
Please wait, while we are loading the content...
Similar Documents
Tabulation-based Induction Proofs with Application to Automated Verification (1998)
| Content Provider | CiteSeerX |
|---|---|
| Author | Roychoudhury, Abhik Ramakrishnan, C. R. Ramakrishnan, I. V. Smolka, S. A. |
| Description | In Workshop on Tabulation in Parsing and Deduction 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... |
| File Format | |
| Language | English |
| Publisher Date | 1998-01-01 |
| Access Restriction | Open |
| Subject Keyword | Automated Verification Whereas Prolog Tabulation-based Induction Proof Program Xsb Tabled Resolution Many Program Logic Programming Predicate Invocation Tabled Predicate Tight Integration Horn Program Equivalent Invocation First One Non-monotonic Reasoning Nmr Paradigm Complexity Property Sld Evaluation Mechanism Poor Termination Deductive Database Tabled Logic Programming System Particular Predicate |
| Content Type | Text |
| Resource Type | Article |
