Online Justification for Tabled Logic Programs
Lecture notes in computer sciencePublished 1 January 2004
Giridhar Pemmasani, Hai-Feng Guo, Yifei Dong, C. R. Ramakrishnan, I. V. Ramakrishnan
Citations31
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper introduces online justification, based on program transformation, to efficiently construct the evidence during query evaluation, while adding little overhead to the evaluation itself, to demonstrate the scalability of online justification.
Abstract
Justification is the process of constructing evidence, in terms of proof, for the truth or falsity of an answer derived by tabled evaluation. The evidence is most easily constructed by post-processing the memo tables created during query evaluation. In this paper we introduce online justification, based on program transformation, to efficiently construct the evidence during query evaluation, while adding little overhead to the evaluation itself. Apart from its efficiency, online justification separates evidence generation from exploration thereby providing flexibility in exploring the evidence either declaratively or procedurally. We present experimental results obtained on examples that construct large evidences which demonstrate the scalability of online justification.
Keywords
Computer Science
Foundations of Logic Programming
4,159 Citations1984John W. Lloyd
Efficient generation of counterexamples and witnesses in symbolic model checking
220 Citations1995E. M. Clarke, Orna Grümberg +2 more
An efficient algorithm to produce counter-examples and witnesses for symbolic model checking algorithms is described, used in the SMV model checker and works quite well in practice.
New Generation ComputingDeclarative error diagnosis
115 Citations1987John W. Lloyd
An error diagnoser which finds errors in logic programs which use the extended syntax and advanced control facilities is presented, arguing that declarative error diagnosers will be indispensable components of advanced logic programming systems, which are currently under development.
Algorithmic program diagnosis
99 Citations1982Ehud Shapiro
Algorithms for detecting incorrect procedures are developed and their performance suggests that the algorithms can be the backbone of debugging aids that go far beyond what is offered by current programming environments.
Lecture notes in computer scienceAnalysis and Visualization Tools for Constraint Programming
86 Citations2000Pierre Deransart, MaÅuszyÅski, Jan +1 more
One of the main features of the preprocessor the authors present is that assertions are optional and can state partial specifications, which raises questions regarding issues such as, for which parts of the program should one write check assertions, what kinds of assertions should be used for a given objective, which kind of properties should been used in a given assertion, etc.
Lecture notes in computer scienceA Simple Scheme for Implementing Tabled Logic Programming Systems Based on Dynamic Reordering of Alternatives
60 Citations2001Hai-Feng Guo, Gopal Gupta
This work presents a simple technique for incorporating tabling in existing LP systems based on dynamically reordering clauses containing variant calls at run-time that allows tabled evaluation to be performed with a single SLD tree and without the use of complex operations such as freezing of stacks and heap.
Lecture notes in computer scienceXMC: A Logic-Programming-Based Verification Toolset
57 Citations2000C. R. Ramakrishnan, I. V. Ramakrishnan +5 more
The core computational components of theXMC system, such as those for compiling the specification language, model checking, etc., are built on top of the XSB tabled logic-programming system.
Lecture notes in computer scienceCombined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs
55 Citations2000Germán Puebla, Francisco Bueno +1 more
A general framework for assertion-based debugging of constraint logic programs and provides techniques for using information from global analysis both to detect at compile-time assertions which do not hold in at least one of the possible executions and assertions which hold for all possible executions.
Lecture notes in computer scienceBeyond depth-first: Improving tabled logic programs through alternative scheduling strategies
53 Citations1996Juliana Freire, Terrance Swift +1 more
Tabled evaluations ensure termination of logic programs with finite models by keeping track of which subgoals have been called, and use of answer resolution prevents infinite looping which happens in SLD.
Justifying proofs using memo tables
41 Citations2000Abhik Roychoudhury, C. R. Ramakrishnan +1 more
This paper proposes the concept of justi er for extracting suAEcient evidence for the truth or falsehood of literals in a logic program, by post-processing the memo tables created during query evaluation, and shows how to constructevidence for the presence/absence of tableau in a tableau-based proof system.
An abstract machine for SLG resolution: definite programs
33 Citations1994Terrance Swift, David S. Warren
Lecture notes in computer scienceA Framework for Assertion-based Debugging in Constraint Logic Programming
19 Citations1998Germán Puebla, Francisco Bueno +1 more
The proposed framework does not wish to limit the programming language or the language of assertions unnecessarily in order to make the assertions statically decidable, but the proposed framework needs to deal throughout with approximations.
ViMer
15 Citations2003M H Cameron, María García de la Banda +2 more
ViMer uses incremental constraint-solving to efficiently draw and incrementally update the visualization of the execution tree, and borrows techniques from standard tracers that help keep the tool efficient while still providing enough information for debugging.
Lecture notes in computer scienceSpeculative Beats Conservative Justification
14 Citations2001Hai-Feng Guo, C. R. Ramakrishnan +1 more
This paper introduces the concept of a speculative justifier, a justifier that select literals that can possibly provide evidence for the goal's truth, assume that their truth values correspond to thegoal's and proceed to build a justification for each of them.
Lecture notes in computer scienceEvidence Explorer: A Tool for Exploring Model-Checking Proofs
13 Citations2003Yifei Dong, C. R. Ramakrishnan +1 more
The Evidence Explorer enables users to explore evidence through a collection of orthogonal but coordinated views, which allow one to quickly ascertain the overall perception of evidence through consistent visual cues, and easily locate interesting regions by simple drill-down operations.
The MIT Press eBooksGenerating Deductive Database Explanations
12 Citations1999Sarah Mallet, Mireille Ducassé
This article describes a technique to generate explanations by integrating a relational trace and an instru-mented meta-interpreter, which enables powerful explanation systems to be implemented with very few modiications of the deductive database mechanism itself.
Lecture notes in computer scienceGeneration of All Counter-Examples for Push-Down Systems
10 Citations2003Samik Basu, Diptikalyan Saha +2 more
A new, on-the-fly algorithm is presented that given a push-down model representing a sequential program with (recursive) procedure calls and an extended finite-state automaton representing (the negation of) a safety property, produces a succinct, symbolic representation of all counter-examples; i.e., traces of system behaviors that violate the property.
UNSWorks (UNSW Sydney)Forced simulation : a formal approach to component based development of embedded systems
7 Citations2000Parthasarathi Roop