Abstract
In [19] we introduced a graphical representation of quantifier-free predicate calculus formulas and a new rule of inference which employs this representation. The new rule is an amalgamation of resolution and Prawitz analysis, which we call path resolution.
Some (but not all) path resolution operations allow the deletion of some links used in the inference and yet preserve the spanning property. We characterize those situations in which links may be so deleted. A spanning-preserving restriction on the inheritance of certain links is also developed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.B. Refutations by matings. IEEE Transactions on Computers 25,8 (Aug. 1976), 801–807.
Andrews, P.B. Theorem proving via general matings. JACM 28,2 (April 1981), 193–214.
Bibel, W. On matrices with connections. JACM 28,4 (Oct. 1981), 633–645.
Bibel, W. A Strong Completeness Result for the Connection Graph Proof Procedure. Technical Report ATP-3-IV-80.
Chang, C.L. and Lee, R.C.T. Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1978.
Chang, C.L., and Slagle, J.R. Using rewriting rules for connection graphs to prove theorems. Artificial Intelligence 12 (Aug. 1979), 159–178.
Chinlund, T.J., Davis, M., Hineman, P.G., and McIlroy, M.D. Theorem proving by matching. Bell Laboratory, 1964.
Clark, K. The Synthesis and Verification of Logic Programs. Third Conference on Automated Deduction, August 1977.
Davis, M. and Putnam, H. A computing procedure for quantification theory. JACM, vol. 7 (1960), 201–215.
Davis, M. Eliminating the irrelevant from mechanical proofs. Proc. Symp. of Applied Mathematics 15 (1963), 15–30.
de Champeaux, D. Sub-problem finder and instance checker — two cooperating processors for theorem provers. Proc. 4th Workshop on Automated Deduction, Austin, Texas, Feb. 1979, 110–114.
Gilmore, P.C., A Proof method for quantification theory. IBM Journal of Research and Development, vol. 4 (1960), 28–35.
Henschen, L.G. Theorem proving by covering expressions. J.ACM, 26,3 (July 1979), 385–400.
Kowalski, R. A proof procedure using connection graphs. J.ACM 22,4 (Oct. 1975), 572–595.
McCharen, J., Overbeek, R. and Wos, L. Problems and experiments for and with automated theorem-proving programs. IEEE Transactions on Computers, C-25,8 (Aug. 1976), 773–782.
Murray, N.V. Completely non-clausal theorem proving. Artificial Intelligence 18,1 (Jan. 1982), 67–85.
Murray, N.V. An experimental theorem prover using fast unification and vertical path graphs. Fourth National Conf. of Canadian Society of Computational Studies of Intelligence, U. of Saskatchewan, May 1982.
Murray, N.V. and Rosenthal, E. Semantic graphs. Technical Report 84-12, Department of Computer Science, SUNY at Albany, Nov. 1984.
Murray, N.V. and Rosenthal, E. Path Resolution and Semantic Graphs. To appear in the proceedings of EUROCAL '85, Linz Austria, April 1–3, 1985.
Nilsson, N.J. A production system for automatic deduction. Technical Note 148, SRI International, 1977.
Prawitz, D. An improved proof procedure. Theoria 26 (1960), 102–139.
Robinson, G.A. and Wos, L. Paramodulation and theorem proving in first order theories with equality. Machine Intelligence 4, 1969, Edinburgh University Press.
Robinson, J.A. A machine oriented logic based on the resolution principle. J.ACM 12,1 (1965), 23–41.
Robinson, J.A. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1 (1965), 227–234.
Robinson, J.A. ”Theoretical Approaches to Non-Numerical Problem Solving,” Springer-Verlag, New York, Inc., 1970, 2–20.
Stickel, M.L. A nonclausal connection-graph resolution theorem-proving program. Proc. AAAI-82 Nat. Conf. on Artificial Intelligence, Pittsburgh, Pennsylvania, Aug. 1982, 229–233.
Waldinger, R. and Manna, Z. A deductive approach to program synthesis. ACM TOPLAS 2,1 (1980), 90–121.
Wos, L., Carson, D. and Robinson, G. Efficiency and completeness of the set of support strategy in theorem proving. J.ACM 12,4 (1965), 536–541.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Murray, N.V., Rosenthal, E. (1986). On deleting links in semantic graphs. In: Calmet, J. (eds) Algebraic Algorithms and Error-Correcting Codes. AAECC 1985. Lecture Notes in Computer Science, vol 229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16776-5_745
Download citation
DOI: https://doi.org/10.1007/3-540-16776-5_745
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16776-1
Online ISBN: 978-3-540-39855-4
eBook Packages: Springer Book Archive