Abstract
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the basic strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences. Finally, we discuss experimental data obtained from a modification of Otter.
Partially supported by NSF Grant No. CCR-8901322.
Partially supported by NSF grants CCR-8901647 and CCR-8814339.
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.
Similar content being viewed by others
References
L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 427–441, Berlin, 1990. Springer-Verlag.
L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1991. To appear in Journal of Logic and Computation.
L. Bachmair. Canonical Equational Proofs. Birkhauser Boston, Inc., Boston MA (1991).
L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic Paramodulation and Superposition. Technical Report No. 92-001, Boston University, Boston, MA, 1992.
D. Brand. Proving theorems with the modification method. SIAM Journal of Computing 4:4 (1975) pp. 412–430.
M. Fay. First-order unification in an equational theory. In Proc. 4th Workshop on Automated Deduction, Austin, Texas (1979).
J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. J. ACM 38:3 (July 1991) pp. 559–587.
J.-M. Hullot. Canonical forms and unification. In Proc. 5th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 87, pp. 318–334, Berlin, 1980. Springer-Verlag.
W. Nutt, P. Réty, and G. Smolka. Basic Narrowing Revisited. Reprinted in Unification, C. Kirchner (ed.), Academic Press, London (1990).
W. McCune. Skolem functions and equality in automated deduction. In Proc. 8th Nat. Conf. on AI, MIT Press, 1990, pp. 246–251.
W. McCune. OTTER 2.0 users guide. Technical Report ANL-90/9, Argonne National Laboratory, Argonne IL, 1990.
X. Nie and D. Plaisted. A complete semantic back-chaining proof system. In Proc. 10th Int. Conf. on Automated Deduction, Lect. Notes in Comput. Sci., vol. 449, pp. 16–27, Berlin, 1990. Springer-Verlag.
J. Pais and G. Peterson. Using forcing to prove completeness of resolution and paramodulation. J. Symbolic Computation 11 (1991) pp. 3–19.
F. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning 2 (1986) pp. 191–216.
G. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing 12 (1983) pp. 82–100.
P. Rety. Improving basic narrowing techniques. In P. Lescanne, editor, Proc. of 2nd Int. Conf. on Rewrite Techniques and Applications, LNCS vol. 256, pp. 228–241, Berlin, 1987. Springer-Verlag.
G.A. Robinson and L. T. Wos. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence 4 pp. 133–150. American Elsevier, New York, 1969.
J. Slagle. Automated theorem proving with simplifiers, commutativity, and associativity. J. ACM 21 (1974) pp. 622–642.
M. Smith and D. Plaisted. Term-rewriting techniques for logic programming I: completion. Report TR88-019, Department of Computer Science, Univ. North Carolina (1988).
W. Snyder and C. Lynch. Goal directed strategies for paramodulation. In Proc. 4th Int. Conf. on Rewriteing Techniques and Applications, Lect. Notes in Comput. Sci., vol. 488, pp. 150–161, Berlin, 1991. Springer-Verlag.
W. Snyder. A Proof Theory for General Unification. Birkhauser Boston, Inc., Boston MA (1991).
L. T. Wos, G. A. Robinson, D. F. Carson, and L. Shalla. The concept of demodulation in theorem proving. Journal of the ACM, Vol. 14, pp. 698–709, 1967.
L. Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, New Jersey, 1988.
H. Zhang. 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
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W. (1992). Basic paramodulation and superposition. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_185
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_185
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive