Automatic Recognition of Tractability in Inference Relations


Autoria(s): McAllester, David
Data(s)

04/10/2004

04/10/2004

01/02/1990

Resumo

A procedure is given for recognizing sets of inference rules that generate polynomial time decidable inference relations. The procedure can automatically recognize the tractability of the inference rules underlying congruence closure. The recognition of tractability for that particular rule set constitutes mechanical verification of a theorem originally proved independently by Kozen and Shostak. The procedure is algorithmic, rather than heuristic, and the class of automatically recognizable tractable rule sets can be precisely characterized. A series of examples of rule sets whose tractability is non-trivial, yet machine recognizable, is also given. The technical framework developed here is viewed as a first step toward a general theory of tractable inference relations.

Formato

3835574 bytes

1506645 bytes

application/postscript

application/pdf

Identificador

AIM-1215

http://hdl.handle.net/1721.1/6528

Idioma(s)

en_US

Relação

AIM-1215