Detecting Unsolvable Queries for Definite Logic Programs

Simple item page
dc.creatorBruynooghe, Maurice
dc.creatorVandecasteele, Henk
dc.creatorde Waal, D. Andre
dc.creatorDenecker, Marc
dc.date2000-03-17
dc.date.accessioned2026-07-07T03:16:06Z
dc.date.available2026-07-07T03:16:06Z
dc.descriptionIn solving a query, the SLD proof procedure for definite programs sometimes searches an infinite space for a non existing solution. For example, querying a planner for an unreachable goal state. Such programs motivate the development of methods to prove the absence of a solution. Considering the definite program and the query ``<- Q'' as clauses of a first order theory, one can apply model generators which search for a finite interpretation in which the program clauses as well as the clause ``false <- Q'' are true. This paper develops a new approach which exploits the fact that all clauses are definite. It is based on a goal directed abductive search in the space of finite pre-interpretations for a pre-interpretation such that ``Q'' is false in the least model of the program based on it. Several methods for efficiently searching the space of pre-interpretations are presented. Experimental results confirm that our approach find solutions with less search than with the use of a first order model generator.
dc.description32 pages including appendix. A preliminary version appeared in proceedings PLILP/ALP98 (Springer LNCS 1490) This version, without appendix appeared in Journal Functional and Logic Programming 1999
dc.identifierhttps://arxiv.org/abs/cs/0003067
dc.identifierhttp://arxiv.org/abs/cs/0003067
dc.identifierJournal of Functional and Logic Programming, Vol. 1999, 1-35, 1999
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/30225
dc.subjectLogic in Computer Science
dc.subjectArtificial Intelligence
dc.subjectD.1.6; F.3.1; F.4.1
dc.titleDetecting Unsolvable Queries for Definite Logic Programs
dc.typetext

Files

Collections

arXiv