{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:44:59Z","timestamp":1725486299833},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441274"},{"type":"electronic","value":"9783540461487"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46148-5_25","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T22:31:45Z","timestamp":1181169105000},"page":"243-252","source":"Crossref","is-referenced-by-count":1,"title":["Towards Semantic Goal-Directed Forward Reasoning in Resolution"],"prefix":"10.1007","author":[{"given":"Seungyeob","family":"Choi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,8,21]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"M. Brown and G. Sutcliffe. PTTP+GLiDeS: Semantically guided PTTP. In D. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17), LNAI 1831, 411\u2013416. Springer-Verlag, 2000.","DOI":"10.1007\/10721959_32"},{"key":"25_CR2","unstructured":"M. Brown and G. Sutcliffe. PTTP+GLiDeS: Using models to guide linear deductions. In Peter Baumgartner et al., editors, Proceedings of Workshop on Model Computation-Principles, Algorithms, and Applications, CADE-17, 42\u201345, 2000."},{"key":"25_CR3","unstructured":"R. Caferra and N. Peltier. Disinference rules, model building and abduction. In E. Or\u0142owska, editor, Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, 331\u2013353. Physica-Verlag, 1999."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"H. Chu and D.A. Plaisted. Semantically guided first-order theorem proving using hyper-linking. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction (CADE-12), LNAI 814, 192\u2013206. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_14"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"N. Eisinger and H.J. Ohlbach. The Markgraf Karl Refutation Procedure (MKRP). In J. Siekmann, editor, Proceedings of the 8th International Conference on Automated Deduction (CADE-8), LNAI 230, 681\u2013682. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_135"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"R. Hasegawa, H. Fujita, and M. Koshimura. MGTP: A Model Generation Theorem Prover-its advanced features and applications. In D. Galmiche, editor, Proceedings of International Conference TABLEAUX\u201997, LNAI 1227, 1\u201315. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0027401"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"X. Huang et al. KEIM: A toolkit for automated deduction. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction (CADE-12), LNAI 814, 807\u2013810. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_65"},{"key":"25_CR8","unstructured":"M. Kerber and S. Choi. The semantic clause graph procedure. In P. Baumgartner et al., editors, Proceedings of the CADE-17 Workshop on Model Computation-Principles, Algorithms, and Applications, 29\u201337, 2000."},{"key":"25_CR9","unstructured":"M. Kerber and E. Melis. Typical examples in reasoning. In International Conference on Computing and Philosophy, 1992."},{"key":"25_CR10","unstructured":"M. Kerber, E. Melis, and J. Siekmann. Analogical reasoning with typical examples. SEKI Report SR-92-13, Fachbereich Informatik, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1992."},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performance Theorem Prover. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"W. McCune. OTTER 3.0 Reference Manual and Guide. Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, Illinois, USA, 1994.","DOI":"10.2172\/10129052"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"W. McCune. Solution of the Robbins problem. Journal of Automated Reasoning, 19:263\u2013276, 1997.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"F.J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2(2):191\u2013216, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Vampire 1.1. In R. Gor\u00e9 et al., editors, Proceedings of the International Joint Conference on Automated Reasoning, LNAI 2083, 376\u2013380. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_29"},{"issue":"1","key":"25_CR16","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23\u201341, 1965.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"25_CR17","unstructured":"J. Slaney. SCOTT: A Model-Guided Theorem Prover. In Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI-93), pages 109\u2013114, 1993."},{"key":"25_CR18","unstructured":"J. Slaney. FINDER-Finite Domain Enumerator Version 3.0 Notes and Guide. Centre for Information Science Research, Australian National University, Canberra, Australia, July 1995."},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"J. Slaney, E. Lusk, and W. McCune. SCOTT: Semantically Constrained Otter. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction (CADE-12), LNAI 814, 764\u2013768. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_56"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. SPASS & FLOTTER, Version 0.42. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction (CADE-13), LNAI 1104, 141\u2013145. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_75"},{"issue":"4","key":"25_CR21","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. A. Robinson, and D. F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the Association for Computing Machinery, 12(4):536\u2013541, 1965.","journal-title":"Journal of the Association for Computing Machinery"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence: Methodology, Systems, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46148-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:45:16Z","timestamp":1556466316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46148-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441274","9783540461487"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46148-5_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}