Superposition with simplification as a decision procedure for the monadic class with equality

• W. Ackermann, 1954. Solvable Cases of the Decision Problem. North-Holland, Amsterdam.

  Google Scholar 

• 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.

  Google Scholar 

• 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.

  Google Scholar 

• 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.

  Google Scholar 

• 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.

  Google Scholar 

• 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.

  Google Scholar 

• 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.

  Google Scholar 

• B. Dreben and W.D. Goldfarb, 1979. The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Inc.

  Google Scholar 

• C. Fermüller, A. Leitsch, T. Tammet and N. Zamov, 1992. Resolution Methods for the Decision Problem. To appear.

  Google Scholar 

• C. Fermüller and G. Salzer, 1993. Ordered Paramodulation and Resolution as Decision Procedure. Submitted.

  Google Scholar 

• N. Heintze and J. Jaffar, 1991. Set-based program analysis. Draft manuscript.

  Google Scholar 

• W. H. Joyner Jr., 1976. Resolution Strategies as Decision Procedures. Journal of the ACM, Vol. 23, No. 3, pp. 398–417.

  Google Scholar 

• H. R. Lewis, 1980. Complexity Results for Classes of Quantificational Formulas. Journal of Computer and System Sciences, Vol. 21, pp. 317–353.

  Google Scholar 

• L. Löwenheim, 1915. Über Möglichkeiten im Relativkalkül. Math. Annalen, Vol. 76, pp. 228–251.

  Google Scholar 

• 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.

  Google Scholar 

• P. Nivela and R. Nieuwenhuis, 1993. Practical results on saturation of full first-order clauses: Experiments with the Saturate system. Submitted.

  Google Scholar 

• M. Rusinowitch, 1989. Démonstration Automatique: Techniques de Réécriture. Intereditions, Paris, France.

  Google Scholar 

• 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.

  Google Scholar 

Download references