@inproceedings{5e5a13643a164ec3b6776be27f76aa7c,
title = "A logical characterization of forward and backward chaining in the inverse method",
abstract = "The inverse method is a generalization of resolution that can be applied to non-classical logics. We have recently shown how Andreoli's focusing strategy can be adapted for the inverse method in linear logic. In this paper we introduce the notion of focusing bias for atoms and show that it gives rise to forward and backward chaining, generalizing both hyperresolution (forward) and SLD resolution (backward) on the Horn fragment. A key feature of our characterization is the structural, rather than purely operational, explanation for forward and backward chaining. A search procedure like the inverse method is thus able to perform both operations as appropriate, even simultaneously. We also present experimental results and an evaluation of the practical benefits of biased atoms for a number of examples from different problem domains.",
author = "Kaustuv Chaudhuri and Frank Pfenning and Greg Price",
year = "2006",
month = jan,
day = "1",
doi = "10.1007/11814771\_9",
language = "English",
isbn = "3540371877",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "97--111",
booktitle = "Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings",
note = "Third International Joint Conference on Automated Reasoning, IJCAR 2006 ; Conference date: 17-08-2006 Through 20-08-2006",
}