Automatic Recognition of Tractability in Inference Relations
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 se...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6528 |
| _version_ | 1826188649945890816 |
|---|---|
| author | McAllester, David |
| author_facet | McAllester, David |
| author_sort | McAllester, David |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T08:02:55Z |
| id | mit-1721.1/6528 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:02:55Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/65282019-04-09T16:17:32Z Automatic Recognition of Tractability in Inference Relations McAllester, David 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. 2004-10-04T15:14:43Z 2004-10-04T15:14:43Z 1990-02-01 AIM-1215 http://hdl.handle.net/1721.1/6528 en_US AIM-1215 3835574 bytes 1506645 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | McAllester, David Automatic Recognition of Tractability in Inference Relations |
| title | Automatic Recognition of Tractability in Inference Relations |
| title_full | Automatic Recognition of Tractability in Inference Relations |
| title_fullStr | Automatic Recognition of Tractability in Inference Relations |
| title_full_unstemmed | Automatic Recognition of Tractability in Inference Relations |
| title_short | Automatic Recognition of Tractability in Inference Relations |
| title_sort | automatic recognition of tractability in inference relations |
| url | http://hdl.handle.net/1721.1/6528 |
| work_keys_str_mv | AT mcallesterdavid automaticrecognitionoftractabilityininferencerelations |