A shortest path algorithm to find minimal deduction graphs

摘要

A new method using a shortest path algorithm to find a minimal deduction graph (MDG) for solving the interference problem is proposed in this article. Let R be a set of nonredundant and nonrecursive function-free rules. Given a source and a sink, a Horm formula (HF) of the form (sink←source) is provable from an MDG(source, sink). This MDG is constructed from the source to the sink in two steps by the proposed algorithm if the MDG exists. HFs are extended from Horn clauses (HC). The first step prepares the connected directed graph representing the candidate set Rc of R with respect to the given sink as the input of the next step. The second one employs the proposed algorithm to construct an MDG(source, sink) for accomplishing the above inference. The utilization of the candidate set Rc of R saves both time and space during the inference process. This shortest path algorithm provide a systematic way to solve the inference problem in a polynomial time with the minimum number of rules and instances of rules. In addition, the algorithm can also automatically detect any extraneous predicates in a given compound source.