Abstract
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.
This research was supported in part by the National Science Foundation under grants CCR-9404338 and CCR-9504349 and by the Deutsche Forschungsgemeinschaft within Schwerpunktprogramm Deduktion.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Anderson and W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. JACM, 17(3):525–534, July 1970.
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.
W. Bibel. On matrices with connections. JACM, 28:633–645, 1981.
W. Bibel and E. Eder. Decomposition of tautologies into regular formulas and strong completeness of connection graph resolution. JACM, 44(2):320–344, 1997.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. CACM, 5:394–397, 1962.
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.
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.
R. Kowalski. A proof procedure using connection graphs. JACM, 22(4):572–595, 1975.
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.
N. V. Murray and E. Rosenthal. Inference with path resolution and semantic graphs. JACM, 34(2):225–254, 1987.
N. V. Murray and E. Rosenthal. Dissolution: Making paths vanish. JACM, 40(3):504–535, 1993.
J. A. Robinson. The generalized resolution principle. In Machine Intelligence, volume 3, pages 77–93. Oliver and Boyd, Edinburgh, 1968.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hähnle, R., Murray, N.V., Rosenthal, E. (1998). Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_21
Download citation
DOI: https://doi.org/10.1007/3-540-69778-0_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64406-4
Online ISBN: 978-3-540-69778-7
eBook Packages: Springer Book Archive