{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171512},"publisher-location":"Berlin\/Heidelberg","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022557","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:14:45Z","timestamp":1131862485000},"page":"83-96","source":"Crossref","is-referenced-by-count":38,"title":["Superposition with simplification as a decision procedure for the monadic class with equality"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"W. Ackermann, 1954. Solvable Cases of the Decision Problem. North-Holland, Amsterdam."},{"key":"11_CR2","first-page":"329","volume-title":"Solving Systems of Set Constraints (Extended Abstract)","author":"A. Aiken","year":"1992","unstructured":"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\u2013340. IEEE Computer Society Press."},{"key":"11_CR3","series-title":"LNAI 449","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"10th International Conference on Automated Deduction","author":"L. Bachmair","year":"1990","unstructured":"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\u2013441. Springer-Verlag."},{"key":"11_CR4","volume-title":"Technical Report MPI-I-91-208","author":"L. Bachmair","year":"1991","unstructured":"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\u00fcr Informatik, Saarbr\u00fccken. Revised version to appear in Journal of Logic and Computation."},{"key":"11_CR5","volume-title":"Technical Report MPI-I-92-240","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger and U. Waldmann, 1992. Set Constraints are the Monadic Class. Technical Report MPI-I-92-240, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. Revised version to appear in Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, 1993."},{"key":"11_CR6","first-page":"255","volume-title":"Decidable Problems in Shallow Equational Theories (Extended Abstract)","author":"H. Comon","year":"1992","unstructured":"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\u2013265. IEEE Computer Society Press."},{"key":"11_CR7","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"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\u2013320. Elsevier Science Publishers B.V., Amsterdam, New York, Oxford, Tokyo."},{"key":"11_CR8","unstructured":"B. Dreben and W.D. Goldfarb, 1979. The Decision Problem. Solvable Classes of Quantificational Formulas. Addison-Wesley Publishing Company, Inc."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet and N. Zamov, 1992. Resolution Methods for the Decision Problem. To appear.","DOI":"10.1007\/3-540-56732-1"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller and G. Salzer, 1993. Ordered Paramodulation and Resolution as Decision Procedure. Submitted.","DOI":"10.1007\/3-540-56944-8_47"},{"key":"11_CR11","unstructured":"N. Heintze and J. Jaffar, 1991. Set-based program analysis. Draft manuscript."},{"issue":"No.3","key":"11_CR12","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner Jr.","year":"1976","unstructured":"W. H. Joyner Jr., 1976. Resolution Strategies as Decision Procedures. Journal of the ACM, Vol. 23, No. 3, pp. 398\u2013417.","journal-title":"Journal of the ACM"},{"key":"11_CR13","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H. R. Lewis","year":"1980","unstructured":"H. R. Lewis, 1980. Complexity Results for Classes of Quantificational Formulas. Journal of Computer and System Sciences, Vol. 21, pp. 317\u2013353.","journal-title":"Journal of Computer and System Sciences"},{"key":"11_CR14","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/BF01458217","volume":"76","author":"L. L\u00f6wenheim","year":"1915","unstructured":"L. L\u00f6wenheim, 1915. \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl. Math. Annalen, Vol. 76, pp. 228\u2013251.","journal-title":"Math. Annalen"},{"key":"11_CR15","series-title":"LNAI 607","first-page":"477","volume-title":"11th International Conference on Automated Deduction","author":"R. Nieuwenhuis","year":"1992","unstructured":"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\u2013491. Springer-Verlag."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"P. Nivela and R. Nieuwenhuis, 1993. Practical results on saturation of full first-order clauses: Experiments with the Saturate system. Submitted.","DOI":"10.1007\/3-540-56868-9_33"},{"key":"11_CR17","volume-title":"D\u00e9monstration Automatique: Techniques de R\u00e9\u00e9criture","author":"M. Rusinowitch","year":"1989","unstructured":"M. Rusinowitch, 1989. D\u00e9monstration Automatique: Techniques de R\u00e9\u00e9criture. Intereditions, Paris, France."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1016\/S0747-7171(08)80131-9"}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022557.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:48:59Z","timestamp":1607550539000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0022557","relation":{},"subject":[]}}