Abstract
Proving failure of queries for definite logic programs can be done by constructing a finite model of the program in which the query is false. A general purpose model generator for first order logic can be used for this. A recent paper presented at PLILP98 shows how the peculiarities of definite programs can be exploited to obtain a better solution. There a procedure is described which combines abduction with tabulation and uses a meta-interpreter for heuristic control of the search. The current paper shows how similar results can be obtained by direct execution under the standard tabulation of the XSB-Prolog system. The loss of control is compensated for by better intelligent backtracking and more accurate failure analysis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Bruynooghe. Solving combinatorial search problems by intelligent backtracking. Information Processing Letters, 12(1):36–39, Feb. 1981.
M. Bruynooghe, H. Vandecasteele, D. A. de Waal, and M. Denecker. Detecting unsolvable queries for definitive logic programs. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming, 10th International Symposium, volume 1490 of Lecture Notes in Computer Science, pages 118–133. Springer Verlag, Sept. 1998.
M. Bruynooghe, H. Vandecasteele, D. A. de Waal, and M. Denecker. Detecting unsolvable queries for definitive logic programs. Journal of Functional and Logic Programming, 1999. To Appear.
W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20–74, Jan. 1996.
M. Codish and B. Demoen. Analyzing logic programs using “PROP”-ositional logic programs and a magic wand. Journal of Logic Programming, 25(3):249–274, Dec. 1995.
J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, second edition, 1987.
N. Peltier. A new method for automated finite model building exploiting failures and symmetries. Journal of Logic and Computation, 8(4):511–543, 1998.
J. A. Robinson. Automatic deduction with hyper-resolution. Int. Journal of Computer Math., 1:227–234, 1965.
K. Sagonas, T. Swift, and D. S. Warren. XSB as an efficient deductive database engine. SIGMOD Record (ACM Special Interest Group on Management of Data), 23(2):442–453, June 1994.
J. Slaney. Finder version 3.0-notes and guides. Technical report, Centre for Information Science Research, Australian National University, July 1995.
C. B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.1.0). Report AR-97-04, Fakultät für Informatik der Technischen Universität München, 1997.
J. Zhang and H. Zhang. SEM: a system for enumerating models. In C. S. Mellish, editor, Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pages 298–303, San Mateo, Aug. 1995. Morgan Kaufmann.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pelov, N., Bruynooghe, M. (1999). Proving Failure of Queries for Definite Logic Programs Using XSB-Prolog. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds) Logic for Programming and Automated Reasoning. LPAR 1999. Lecture Notes in Computer Science(), vol 1705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48242-3_22
Download citation
DOI: https://doi.org/10.1007/3-540-48242-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66492-5
Online ISBN: 978-3-540-48242-0
eBook Packages: Springer Book Archive