Polynomial-time Computation via Local Inference Relations

TL;DR

This paper introduces a method to transform local inference rule sets into polynomial-time evaluation strategies, enabling efficient reasoning for a broad class of rule sets and exploring the limits of locality in inference systems.

Contribution

It demonstrates that all polynomial-time predicates can be defined by local rule sets, identifies a machine-recognizable subclass, and proves that locality is undecidable in general.

Findings

Every polynomial-time predicate can be defined by an unstratified local rule set.

A new machine-recognizable subclass of local rule sets is identified.

Locality as a property of rule sets is undecidable in general.

Abstract

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 cannot 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.