Abstract
We show that superposition, a restricted form of paramodulation, can be combined with specifically designed simplification rules such that it becomes a decision procedure for the monadic class with equality. The completeness of the method follows from a general notion of redundancy for clauses and superposition inferences.
The research described in this paper was supported in part by the German Science Foundation (Deutsche Forschungsgemeinschaft) under grant Ga 261/4-1, by the German Ministry for Research and Technology (Bundesministerium für Forschung und Technologie) under grant ITS 9102/ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. Ackermann, 1954. Solvable Cases of the Decision Problem. North-Holland, Amsterdam.
A. Aiken and E. L. Wimmers, 1992. Solving Systems of Set Constraints (Extended Abstract). In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, USA, pp. 329–340. IEEE Computer Society Press.
L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, LNAI 449, pp. 427–441. Springer-Verlag.
L. Bachmair and H. Ganzinger, 1991. Rewrite-Based Equational Theorem Proving With Selection and Simplification. Technical Report MPI-I-91-208, Max-Planck-Institut für Informatik, Saarbrücken. Revised version to appear in Journal of Logic and Computation.
L. Bachmair, H. Ganzinger and U. Waldmann, 1992. Set Constraints are the Monadic Class. Technical Report MPI-I-92-240, Max-Planck-Institut für Informatik, Saarbrücken. Revised version to appear in Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, 1993.
H. Comon, M. Haberstrau and J.-P. Jouannaud, 1992. Decidable Problems in Shallow Equational Theories (Extended Abstract). In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, USA, pp. 255–265. IEEE Computer Society Press.
N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, chapter 6, pp. 243–320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo.
B. Dreben and W.D. Goldfarb, 1979. The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Inc.
C. Fermüller, A. Leitsch, T. Tammet and N. Zamov, 1992. Resolution Methods for the Decision Problem. To appear.
C. Fermüller and G. Salzer, 1993. Ordered Paramodulation and Resolution as Decision Procedure. Submitted.
N. Heintze and J. Jaffar, 1991. Set-based program analysis. Draft manuscript.
W. H. Joyner Jr., 1976. Resolution Strategies as Decision Procedures. Journal of the ACM, Vol. 23, No. 3, pp. 398–417.
H. R. Lewis, 1980. Complexity Results for Classes of Quantificational Formulas. Journal of Computer and System Sciences, Vol. 21, pp. 317–353.
L. Löwenheim, 1915. Über Möglichkeiten im Relativkalkül. Math. Annalen, Vol. 76, pp. 228–251.
R. Nieuwenhuis and A. Rubio, 1992. Theorem Proving with Ordering Constrained Clauses. In D. Kapur, editor, 11th International Conference on Automated Deduction, Saratoga Springs, New York, USA, LNAI 607, pp. 477–491. Springer-Verlag.
P. Nivela and R. Nieuwenhuis, 1993. Practical results on saturation of full first-order clauses: Experiments with the Saturate system. Submitted.
M. Rusinowitch, 1989. Démonstration Automatique: Techniques de Réécriture. Intereditions, Paris, France.
M. Rusinowitch, 1991. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix completion procedure as a complete set of inference rules. Journal of Symbolic Computation, Vol. 11.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmair, L., Ganzinger, H., Waldmann, U. (1993). Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022557
Download citation
DOI: https://doi.org/10.1007/BFb0022557
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57184-1
Online ISBN: 978-3-540-47943-7
eBook Packages: Springer Book Archive