CHART PARSERS AS INFERENCE SYSTEMS FOR FIXED-MODE LOGIC PROGRAMS

Logic programs resemble context-free grammars. Moreover, Prolog's proo f procedure can be viewed as a generalization of a simple top-down par ser with backtracking. This simple parser has disadvantages that motiv ated the design of more sophisticated parsing methods. As similar disa dvantages occur in Prolog's proof procedure, it may be desirable to de velop other proof procedures for logic programs than the one used by P rolog. The resemblance between definite clauses and productions sugges ts looking at parsing to develop such procedures. We obtain proof proc edures for fixed-mode logic programs, based on ''chart'' parsers. Our approach concentrates on transforming (fixed-mode) logic programs rath er than the parser. We first add unification to a chart parser obtaini ng a proof procedure for programs severely restricted in their syntax, in which the body of the clauses denotes the composition of binary re lations: ''chain'' programs. We then show how to transform fixed-mode programs into chain form. We arrive at proof procedures that avoid som e nonterminating loops as well as the recomputation of some partial re sults.