Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion
- 221 Downloads
A new completeness proof that generalizes the Anderson-Bledsoe excess literal argument is developed for connection-graph resolution. The technique also provides a simplified completeness proof for semantic resolution. Some observations about subsumption and about link deletion are made. Link deletion is the basis for connection graphs. Subsumption plays an important role in most resolution-based inference systems. In some settings—for example, connection graphs in negation normal form—both subsumption and link deletion can be quite tricky. Nevertheless, a completeness result that uses both is obtained in this setting.
KeywordsCompleteness Proof Disjunctive Normal Form Unit Clause Semantic Tree Resolution Step
Unable to display preview. Download preview PDF.
- 2.L. Bachmair and H. Ganzinger. A theory of resolution. Technical Report MPI-I-97-2-005, Max-Planck-Institut für Informatik, Saarbrücken, 1997. To appear in: J. A. Robinson & A. Voronkov (eds.), Handbook of Automated Reasoning, Elsevier.Google Scholar
- 6.R. Hähnle, N. Murray, and E. Rosenthal. Completeness for linear regular negation normal form inference systems. In Z. W. Raś and A. Skowron, editors, Found. of Intelligent Systems ISMIS’97, Charlotte/NC, USA, volume 1325 of LNCS, pages 590–599. Springer-Verlag, 1997.Google Scholar
- 7.R. Hähnle, N. Murray, and E. Rosenthal. A remark on proving completeness. In D. Galmiche, editor, Position Papers at Conf. on Analytic Tableaux and Related Methods, Nancy, France, pages 41–47, 1997. Tech. Rep. 97-R-030, CRIN Nancy.Google Scholar
- 9.N. Murray, A. Ramesh, and E. Rosenthal. The semi-resolution inference rule and prime implicate computations. In Proc. Fourth Golden West International Conference on Intelligent Systems, San Fransisco, CA, USA, pages 153–158, June 1995.Google Scholar
- 12.J. A. Robinson. The generalized resolution principle. In Machine Intelligence, volume 3, pages 77–93. Oliver and Boyd, Edinburgh, 1968.Google Scholar
- 13.M. E. Stickel. A nonclausal connection-graph resolution theorem-proving program. In D. Waltz, editor, Proc. National Conference on Artificial Intelligence, pages 229–233, Pittsburgh, PA, Aug. 1982. AAAI Press.Google Scholar