New Results on Local Inference Relations

We consider the concept of a local set of inference rules. A local rule set can be automatically transformed into a rule set for which bottom up evaluation terminates in polynomial time. The local rule set transformation gives polynomial time evaluation strategies for a large variety of rule sets that can not be given terminating evaluation strategies by any other known automatic technique. This paper discusses three new results. First, it is shown that every polynomial time predicate can be defined by an (unstratified) local rule set. Second, a new machine recognizable subclass of the local rule sets is identified. Finally we show that locality, as a property of rule sets, is undecidable in general. This paper appeared in KR-92. A postscript electronic source for this paper can be found in ftp.ai.mit.edu:/pub/dam/kr92.ps. A bibtex reference can be found in internet file ftp.ai.mit.edu:/pub/dam/dam.bib. 1 INTRODUCTION Under what conditions does a given set of inference rules define ..