Abstract
Equality is an important relation and many theorems can be easily symbolized through it's use. But it presents special strategic problems, both theoretical and practical, for theorem proving programs. A proposed inference rule in [6] called HL-resolution is intended to have the benefits of hyper steps while controlling the application of paramodulation. The rule is complete for E-unsatisfiable Horn sets. Here we try to find an efficient procedure for finding all k-pd links between two terms and try to find useful heuristics by making some experiments on ring theory. The linking process makes use of an equality graph which is constructed once at the beginning of the run. Once a pair of candidate terms for HL-resolution is chosen in the search, potential linkages can be found and tested for compatibility efficiently by looking at the paths in the graph. Further we try to find heuristics to prevent redundant k-pd links from being used to generate HL-resolvents. The method has been implemented on an existing theoremproving system. A number of experiments were conducted on problems in abstract algebra and a comparison with set-of-support paramodulation was made.
This work was supported, in part, by the research project 5EU230 of Electronics Telecommunications Research Institute.
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
7. Reference
Blasius, K. H., "Equality Reasoning in Clause Graph," IJCAI, 1983.
Darlington, J. L., "Automated Theorem Proving with Equality Substitutions and Mathematical Induction," in Machine Intelligence, Vol. 3 (B. Meltzer and D. Michie, eds.), American Elsevier, New York, pp. 113–127.
Digricoli, V. J., "Resolution by unification and Equality," Proceedings of 4th Workshop on Automated Deduction, 1979.
Harrison, M. and N. Rubin, "Another Generalization of Resolution," J. ACM, Vol. 25, No. 3, July 1978, pp.341–351.
Lim, Younghwan, A New Hyperparamodulation Strategy for the Equality Clauses, Ph. D. Dissertation at Northwestern University, 1985.
Younghwan Lim and Lawrence J. Henschen, "A New Hyperparamodulation Strategy for the Equality Relation," IJCAI 85, pp. 1138–1145.
McCune, W., Semantic Paramodulation for Horn Sets, Ph.D. Sissertation at Northwestern University, 1984.
Morris, J., "E-resolution: an Extension of Resolution to Include the Equality Relation," IJCAI, 1969.
Overbeek, R., J. McCharen and L. Wos, "Complexity and Related Enhancements for Atomated Theorem-proving Program," Comp. and Maths. with Appls., Vol. 2, No. 1-A, 1976, pp.1–16.
Robinson, G. A. and L. Wos, "Paramodulation and Theorem Proving in First Order Theories with Equality," in Machine Intelligence Vol. 4 (B. Meltzer and D. Michie, eds) Amerian Elsever, New York, 1969, pp.135–150.
Siekmann, J. and G. Wrightson, "Paramoulated Connection Graphs," Acta Informatica, 1980
Wos, L., "Paramodulation and Set of Support," the IRIA Symposium on Automatic Demonstration ar Versailles, 1968.
Wos, L., R. Overbeek and L. Henschen, "HYPERPARAMODULATION: A Refinement of Paramodulation, "Proceedings of the 5th Conference on Automated Deduction, 1980, pp.208–219.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lim, Y. (1986). The heuristics and experimental results of a new hyperparamodulation: HL-resolution. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_94
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_94
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive