Abstract
It is well-known that the set of support strategy is incomplete in paramodulation theorem provers if paramodulation into variables is forbidden. In this paper, we present a paramodulation calculus for which the combination of these two restrictions is complete, based on a lazy form of the paramodulation rule which delays parts of the unification step. The refutational completeness of this method is proved by transforming proofs given by other paramodulation strategies into set of support proofs using this new inference rule. Finally, we consider the completeness of various refinements of the method, and conclude by discussing related work and future directions.
This research was partially supported by NSF Grant No. CCR-8910268.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
5 References
Anderson, R., “Completeness Results for E-Resolution”, Proceedings of the AFIPS Spring Joint Computer Conference, AFIPS Press, Reston, VA (1970) 653–656.
Bachmair, L., “Proof Normalization for Resolution and Paramodulation,” Proceedings of RTA89, Chapel Hill, p. 15–28.
Bachmair, L. and H. Ganzinger, “On Restrictions of Ordered Paramodulation with Simplification,” CADE 1990, Kaiserslautern, Germany.
Brand, D., “Proving Theorems with the Modification Method,” SIAM Journal of Computing 4:4 (1975) 412–430.
Chang, C., and R. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York (1973).
Digricoli, V., and M. Harrison, “Equality-Based Binary Resolution,” JACM 33:2 (April 1986) 253–289.
Dougherty, D., and P. Johann, “An Improved General E-Unification Method,” Proceedings of CADE 1990, Kaiserlautern, Germany.
Gallier, J., Logic for Computer Science: Foundations of Automated Theorem Proving, Harper and Row, New York (1986).
Gallier, J. and W. Snyder, “A General Complete E-Unification Procedure,” Proceedings of RTA 1987, Bordeaux, France.
Gallier, J. and W. Snyder, “Complete Sets of Transformations for General E-Unification,” TCS 67 (1989) 203–260.
Hsiang, J., and M. Rusinowitch, “Proving Refutational Completeness of Theorem Proving Strategies: The Transfinite Semantic Tree Method,” to appear in JACM (1990).
Loveland, D., Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam (1978).
Martelli, A., and U. Montanari, “An Efficient Unification Algorithm,” ACM Transactions on Programming Languages and Systems 4:2 (1982) 258–282.
Morris, J., “E-Resolution: Extensions of Resolution to Include the Equality Relation,” International Joint Conference on Artificial Intelligence, Washington D.C. (1969).
Peterson, G., “A Technique for Establishing Completeness Results in Theorem Proving with Equality,” SIAM Journal of Computing 12 (1983) 82–100.
Plaisted, D., and S. Greenbaum, “Problem Representations for Back Chaining and Equality in Resolution Theorem Proving,” Proceedings of the First Conference on Artificial Intelligence Applications (1984).
Robinson, J., “A Machine Oriented Logic based on the Resolution Principle,” JACM 12 (1965) 23–41.
Robinson, G., and L. Wos, “Paramodulation and Theorem Proving in First-Order Theories with Equality,” Machine Intelligence 4 (1969) 133–150.
Rusinowich, M., Démonstration Automatique: Technique de Réécriture, InterEditions, Paris (1989).
Snyder, W., “Higher-Order E-Unification,” Proceedings of CADE 1990, Kaiserlautern, Germany.
Snyder, W., Complete Sets of Transformations for General Unification, Disseration, University of Pennsylvania (1988). To appear as a book published by Birkhäuser Boston Inc., for their series Progress in Computer Science and Applied Logic.
Snyder, W. and C. Lynch, “Complete Inference Systems for Horn Clause Logic with Equality: A Foundation for Logic Programming with Equality,” Proceedings of Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada (1990).
Stickel, M., Tutorial on Term Rewriting, CADE 1988, Argonne, IL.
Wos, L., G. Robinson, and D. Carson, “Efficiency and Completeness of the Set of Support Strategy in Theorem Proving,” JACM 12:4 (Oct. 1965) 536–541.
Wos, L., and G. Robinson, “Paramodulation and Set of Support,” IRIA Symposium on Automatic Demonstration, Versailles, France (1968).
Zhang, H., Reduction, Superposition, and Induction: Automated Reasoning in an Equational Logic, Ph.D. Thesis, Rensselaer Polytechnic Institute (1988).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Snyder, W., Lynch, C. (1991). Goal directed strategies for paramodulation. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_93
Download citation
DOI: https://doi.org/10.1007/3-540-53904-2_93
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53904-9
Online ISBN: 978-3-540-46383-2
eBook Packages: Springer Book Archive