{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:37Z","timestamp":1725488617828},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_5","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"80-94","source":"Crossref","is-referenced-by-count":4,"title":["Replacement Rules with Definition Detection"],"prefix":"10.1007","author":[{"given":"David A.","family":"Plaisted","sequence":"first","affiliation":[]},{"given":"Yunshan","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Matthew Bishop and Peter B. Andrews. Selectively instantiating Definitions. In Proceedings of the 15th International Conference on Automated Deduction, pages 365\u2013380, 1998.","DOI":"10.1007\/BFb0054272"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BF00881869","volume":"11","author":"W. W. Bledsoe","year":"1991","unstructured":"W. W. Bledsoe and G. Feng. Set-var. Journal of Automated Reasoning, 11(3):293\u2013314, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00245817","volume":"6","author":"D. Cantone","year":"1990","unstructured":"D. Cantone, E.G. Omodeo, and A. Policriti. The automation of syllogistic II: optimization and complexity issues. Journal of Automated Reasoning, 6(2):173\u2013187, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Heng Chu and D. Plaisted. Semantically guided first-order theorem proving using hyper-linking. In Proceedings of the Twelfth International Conference on Automated Deduction, pages 192\u2013206, 1994. Lecture Notes in Artificial Intelligence 814.","DOI":"10.1007\/3-540-58156-1_14"},{"key":"5_CR6","series-title":"Technical Report","volume-title":"Theorem proving modulo","author":"G. Dowek","year":"1998","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Technical Report 3400, Institut National de Recherche en Informatique et en Automatique (INRIA), Le Chesnay, France, April 1998."},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201\u2013215, 1960.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR9","unstructured":"D. Gabbay, J. Ohlbach, and D. Plaisted. Killer transformations. In Proc. 1993 Workshop on Proof Theory in Modal Logic, pages 1\u201345, Hamburg, Germany, 1993."},{"key":"5_CR10","first-page":"217","volume":"1","author":"S.-J. Lee","year":"1994","unstructured":"S.-J. Lee and D. Plaisted. Use of replace rules in theorem proving. Methods of Logic in Computer Science, 1:217\u2013240, 1994.","journal-title":"Methods of Logic in Computer Science"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"W. McCune. Otter 2.0 (theorem prover). In M.E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 663\u20134, July 1990.","DOI":"10.1007\/3-540-52885-7_131"},{"key":"5_CR12","unstructured":"M. Paramasivam. Instance-Based First-Order Methods Using Propositional Calculus Provers. PhD thesis, University of North Carolina at Chapel Hill, 1997."},{"issue":"3","key":"5_CR13","first-page":"352","volume":"11","author":"L.C. Paulson","year":"1992","unstructured":"L.C. Paulson. Set theory for verification I: from foundations to functions. Journal of Automated Reasoning, 11(3):352\u2013390, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0747-7171(08)80136-8","volume":"11","author":"D. Plaisted","year":"1991","unstructured":"D. Plaisted and R Potter. Term rewriting: Some experimental results. Journal of Symbolic Computation, 11:149\u2013180, 1991.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"5_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1023\/A:1005847700447","volume":"18","author":"M. Paramasivam","year":"1997","unstructured":"M. Paramasivam and D. Plaisted. A replacement rule theorem prover. Journal of Automated Reasoning, 18(2):221\u2013226, 1997.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1023\/A:1005866922570","volume":"20","author":"M. Paramasivam","year":"1998","unstructured":"M. Paramasivam and D. Plaisted. Automated deduction techniques for classification in description logics. Journal of Automated Reasoning, 20(3):337\u2013364, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR18","unstructured":"D. Plaisted and Y. Zhu. Ordered semantic hyper linking. In Proceedings of Fourteenth National Conference on Artificial Intelligence (AAAI97), Providence, Rhode Island, 1997."},{"issue":"1","key":"5_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"A. Quaife. Automated deduction in NBG set theory. Journal of Automated Reasoning, 8(1):91\u2013147, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR20","series-title":"Technical Report","volume-title":"The TPTP problem library (TPTP v2.0.0)","author":"C.B. Suttner","year":"1997","unstructured":"C.B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.0.0). Technical Report AR-97-01, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany, 1997."},{"key":"5_CR21","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the Association for Computing Machinery, 12:536\u2013541, 1965.","journal-title":"Journal of the Association for Computing Machinery"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T14:57:54Z","timestamp":1556722674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}