{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:11:41Z","timestamp":1725631901120},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540517436"},{"type":"electronic","value":"9783642751004"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/978-3-642-75100-4_12","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T18:09:29Z","timestamp":1320862169000},"page":"102-106","source":"Crossref","is-referenced-by-count":1,"title":["A Resolution Calculus Extended by Equivalence"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"M\u00fcller","sequence":"first","affiliation":[]},{"given":"Rolf","family":"Socher-Ambrosius","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","volume-title":"of 2nd Conference on Logic in Computer Science","author":"L Bachmair","year":"1987","unstructured":"Bachmair, L. amp; Dershowitz, N. (1987). Inference Rules for Rewrite-Based First Order Theorem Proving. In: Proc. of 2nd Conference on Logic in Computer Science."},{"key":"12_CR2","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"CL Chang","year":"1973","unstructured":"Chang, C.L. amp; Lee, R.C.T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York."},{"key":"12_CR3","volume-title":"University of Illinois at Urbana-Champaign","author":"J Hsiang","year":"1982","unstructured":"Hsiang, J. (1982). Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Dep. of Comp. Sc., University of Illinois at Urbana-Champaign."},{"key":"12_CR4","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Hsiang, J. (1985). Refutational Theorem Proving using Term-rewriting Systems. Artificial Intelligence 25, 255\u2013300.","journal-title":"Artificial Intelligence"},{"key":"12_CR5","volume-title":"Fair Conditional Term Rewriting Systems: Unification","author":"S Kaplan","year":"1984","unstructured":"Kaplan, S. (1984). Fair Conditional Term Rewriting Systems: Unification, Termination, and Confluence. LRI, Orsay."},{"key":"12_CR6","volume-title":"General Electric Corp","author":"D Kapur","year":"1985","unstructured":"Kapur, D. amp; Narendran, P. (1985). An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 84CRD322, General Electric Corp. Research and Development Report, Schenectady, N.Y."},{"key":"12_CR7","volume-title":"Universit\u00e4t Kaiserslautern","author":"K Markgraf","year":"1984","unstructured":"Markgraf, K. (1984). The Markgraf Karl Refutation Procedure. SEKI-Memo MK-84-01, Universit\u00e4t Kaiserslautern."},{"key":"12_CR8","volume-title":"Universit\u00e4t Kaiserslautern","author":"J M\u00fcller","year":"1988","unstructured":"M\u00fcller, J. amp; Socher, R. (1988). Topics in Completion Theorem Proving. SEKI-Report SR-88-13, Universit\u00e4t Kaiserslautern."},{"key":"12_CR9","unstructured":"M\u00fcller, J. amp; Socher, R. (1989). RE-Resolution. SEKI-Report SR-89-??, Universit\u00e4t Kaiserslautern."},{"key":"12_CR10","first-page":"250","volume-title":"Proc. of the 1 lthe German Workshop on Artificial Intelligence, Geseke. Springer IFB 152,241 \u2013","author":"J M\u00fcller","year":"1987","unstructured":"M\u00fcller, J. (1987). Theopogles - A Theorem Prover Based on First-Order Polynomials and a Special Knuth-Bendix Procedure. In: K. Morik (Ed.): Proc. of the 1 lthe German Workshop on Artificial Intelligence, Geseke. Springer IFB 152,241\u2013250."},{"key":"12_CR11","first-page":"63","volume-title":"Proc. of 5th Conf. on Automated Deduction. Springer LNCS 87,50 \u2013","author":"H Noll","year":"1980","unstructured":"Noll, H. (1980). A Note on Resolution: How to Get Rid of Factoring Without Loosing Completeness. In: W. Bibel & R. Kowalski (Eds): Proc. of 5th Conf. on Automated Deduction. Springer LNCS 87,50\u201363."},{"issue":"2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"FJ Pelletier","year":"1986","unstructured":"Pelletier, FJ. (1986). Seventy-five Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning. 2 \/2, 191\u2013216.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR13","first-page":"591","volume-title":"Proceedings of the 9th International Conference on Automated Deduction. Argonne, Illinois, U.S.A. Springer LNCS 310, 582 \u2013","author":"A Rabinov","year":"1988","unstructured":"Rabinov, A. (1988). A Restriction of Factoring in Binary Resolution. In: E. Lusk amp; R. Overbeek (Eds.): Proceedings of the 9th International Conference on Automated Deduction. Argonne, Illinois, U.S.A. Springer LNCS 310, 582\u2013591."},{"key":"12_CR14","unstructured":"Robinson, G. amp; Wos, L. (1969). Paramodulation and theorem-proving in first-order theories with equality. In: B. Meitzer, amp; D. Michie, (Eds.): Machine Intelligence 4. Edinburgh, 135\u2013150."},{"key":"12_CR15","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A. (1965). Automated Deduction with Hyper-Resolution. Intern. Journal of Comp. Mathematics, 1,227 \u2013 234.","journal-title":"Intern. Journal of Comp. Mathematics"},{"key":"12_CR16","volume-title":"D\u00e9monstration automatique par des techniques de r\u00e9\u00e9criture","author":"M Rusinowitch","year":"1987","unstructured":"Rusinowitch, M. (1987). D\u00e9monstration automatique par des techniques de r\u00e9\u00e9criture. Th\u00e8se de doctorat d\u2019etat. Nancy."},{"key":"12_CR17","first-page":"33","volume-title":"Automated Reasoning","author":"L Wos","year":"1988","unstructured":"Wos, L. (1988). Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs."},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"Wos, L. et.al. (1967). The Concept of Demodulation in Theorem Proving. Journal of the ACM, 14,698\u2013709.","journal-title":"Journal of the ACM"},{"key":"12_CR19","first-page":"4","volume-title":"Reveur","author":"H Zhang","year":"1984","unstructured":"Zhang, H. (1984). Reveur 4: Etude et Mise en \u0152uvre de la R\u00e9\u00e9criture Conditionelle. Th\u00e8se de Doctorat de cycle. Universit\u00e9 de Nancy I."},{"key":"12_CR20","first-page":"20","volume-title":"Proceedings of the 9th International Conference on Automated Deduction. Argonne, Illinois, U.S.A. Springer LNCS 310, 1 \u2013","author":"H Zhang","year":"1988","unstructured":"Zhang, H. amp; Kapur, D. (1988). First-Order Theorem Proving Using Conditional Rewrite Rules. In: E. Lusk amp; R. Overbeek (Eds.): Proceedings of the 9th International Conference on Automated Deduction. Argonne, Illinois, U.S.A. Springer LNCS 310, 1\u201320."}],"container-title":["Informatik-Fachberichte","GWAI-89 13th German Workshop on Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-75100-4_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T02:29:47Z","timestamp":1606271387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-75100-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540517436","9783642751004"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-75100-4_12","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1989]]}}}