Detecting Unsolvable Queries for Definite Logic Programs
<|reference_start|>Detecting Unsolvable Queries for Definite Logic Programs: In 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.<|reference_end|>
@article{bruynooghe2000detecting,
    title={Detecting Unsolvable Queries for Definite Logic Programs},
    author={Maurice Bruynooghe (1), Henk Vandecasteele (1), D. Andre de Waal (2),
  Marc Denecker (1) ((1) Katholieke Universiteit Leuven, Belgium, (2)
  Potchefstroom University for Christian Higher Education, South Africa)},
    journal={Journal of Functional and Logic Programming, Vol. 1999, 1-35, 1999},
    year={2000},
    archivePrefix={arXiv},
    eprint={cs/0003067},
    primaryClass={cs.LO cs.AI}
}