{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:20Z","timestamp":1749125180447},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:18Z","timestamp":1330269678000},"page":"192-206","source":"Crossref","is-referenced-by-count":15,"title":["Semantically guided first-order theorem proving using hyper-linking"],"prefix":"10.1007","author":[{"given":"Heng","family":"Chu","sequence":"first","affiliation":[]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"14_CR1","first-page":"3","volume":"10","author":"A. M. Ballantyne","year":"1982","unstructured":"A. M. Ballantyne and W. W. Bledsoe. On generating and using examples in proof discovery. Machine Intelligence, 10:3\u201339, 1982.","journal-title":"Machine Intelligence"},{"key":"14_CR2","unstructured":"W. W. Bledsoe. Using examples to generate instantiations of set variables. In Proc. of the 8th IJCAI, pages 892\u2013901, Karlsruhe, FRG, 1983."},{"key":"14_CR3","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"W. W. Bledsoe. Challenge problems in elementary calculus. J. Automated Reasoning, 6:341\u2013359, 1990.","journal-title":"J. Automated Reasoning"},{"key":"14_CR4","unstructured":"M. Bruschi. The halting problem. AAR Newsletter, March 1991."},{"key":"14_CR5","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Ricardo Caferra and Nicolas Zabel. A method for simutaneous search for refutations and models by equational constaint solving. J. Symbolic Computation, 13:613\u2013641, 1992.","journal-title":"J. Symbolic Computation"},{"key":"14_CR6","volume-title":"PhD thesis","author":"H. Chu","year":"1994","unstructured":"Heng Chu. Semantically Guided First-Order Theorem Proving Using Hyper-Linking. PhD thesis, University of North Carolina at Chapel Hill, 1994. Expected."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Heng Chu and David A. Plaisted. Model finding in semantically guided instanebased theorem proving. Foundamenta Informaticae Journal, 1993. To appear.","DOI":"10.1007\/3-540-56804-2_2"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Heng Chu and David A. Plaisted. Model finding strategies in semantically guided instance-based theorem proving. In Jan Komorowski and Zbigniew W. Ra\u015a, editors, Proceedings of the 7th International Symposium on Methodologies for Intelligent Systems (ISMIS-93), pages 19\u201328, 15\u201318 June 1993.","DOI":"10.1007\/3-540-56804-2_2"},{"key":"14_CR9","unstructured":"Heng Chu and David A. Plaisted. Rough resolution: A refinement of resolution to remove large literals. In Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), pages 15\u201320, 11\u201315 July 1993."},{"key":"14_CR10","unstructured":"Heng Chu and David A. Plaisted. The use of presburger formulas in semantically guided theorem proving. Presented in The Third International Symposium on Artificial Intelligence and Mathematics, January 1994."},{"issue":"3","key":"14_CR11","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. J. ACM, 7(3):201\u2013215, 1960.","journal-title":"J. ACM"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"P. C. Gilmore. A proof method for quantification theory: its justification and realization. IBM J. Res. Dev., pages 28\u201335, 1960.","DOI":"10.1147\/rd.41.0028"},{"key":"14_CR13","unstructured":"J. Herbrand. Researches in the theory of demonstration. In J. van Heijenoort, editor, From Frege to G\u00f6del: a source book in Mathematical Logic, 1879\u20131931, pages 525\u2013581. Harvard Univ. Press, 1974."},{"key":"14_CR14","volume-title":"PhD thesis","author":"S. Lee","year":"1990","unstructured":"Shie-Jue Lee. CLIN: An Automated Reasoning System Using Clause Linking. PhD thesis, University of North Carolina at Chapel Hill, 1990."},{"key":"14_CR15","first-page":"25","volume":"9","author":"S. Lee","year":"1992","unstructured":"Shie-Jue Lee and David. A. Plaisted. Eliminating duplication with the hyper-linking strategy. J. Automated Reasoning, 9:25\u201342, 1992.","journal-title":"J. Automated Reasoning"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Rainer Manthey and Fran\u00e7ois Bry. SATCHMO: a theorem prover implemented in Prolog. In E. Lusk and R. Overbeek, editors, Proc. of CADE-9, pages 415\u2013434, Argonne, IL, 1988.","DOI":"10.1007\/BFb0012847"},{"key":"14_CR17","volume-title":"OTTER 2.0 Users Guide","author":"William W. W. McCune","year":"1990","unstructured":"William W. McCune. OTTER 2.0 Users Guide. Argonne National Laboratory, Argonne, Illinois, March 1990."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Xumin Nie and David A. Plaisted. A complete semantic back chaining proof system. In Mark E. Stickel, editor, Proc. of CADE-10, pages 16\u201327, Kaiserslautern, Germany, 1990.","DOI":"10.1007\/3-540-52885-7_76"},{"key":"14_CR19","doi-asserted-by":"crossref","first-page":"919","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. J. Automated Reasoning, 2:919\u2013216, 1986.","journal-title":"J. Automated Reasoning"},{"key":"14_CR20","doi-asserted-by":"crossref","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. J. Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"J. Symbolic Computation"},{"key":"14_CR21","first-page":"287","volume":"4","author":"David A. A. Plaisted","year":"1988","unstructured":"David A. Plaisted. Non-Horn clause logic programming without contrapositives. J. Automated Reasoning, 4:287\u2013325, 1988.","journal-title":"J. Automated Reasoning"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"David. A. Plaisted, Geoffrey D. Alexander, Heng Chu, and Shie-Jue Lee. Conditional term rewriting and first-order theorem proving. In Proceedings of the Third International Workshop on Conditional Term-Rewriting Systems, Pont-\u00e0-Mousson, France, 8\u201310 July 1992. Invited Talk.","DOI":"10.1007\/3-540-56393-8_19"},{"key":"14_CR23","unstructured":"John K. Slaney and Ewing L. Lusk. Finding models: Techniques and applications. Tutorial in CADE-11, 1992."},{"key":"14_CR24","unstructured":"H. Wang. Formalization and automatic theorem-proving. In Proc. of IFIP Congress 65, pages 51\u201358, Washington, D.C., 1965."},{"key":"14_CR25","unstructured":"Tie Cheng Wang. Designing examples for semantically guided hierarchical deduction. In Proc. of the 9th IJCAI, pages 1201\u20131207, Los Angeles, CA, 1985."},{"key":"14_CR26","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF00381144","volume":"3","author":"T. Wang","year":"1987","unstructured":"Tie-Cheng Wang and W. W. Bledsoe. Hierarchical deduction. J. Automated Reasoning, 3:35\u201377, 1987.","journal-title":"J. Automated Reasoning"},{"key":"14_CR27","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"S. Winker. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. J. ACM, 29:273\u2013284, 1982.","journal-title":"J. ACM"},{"key":"14_CR28","first-page":"5","volume-title":"Automated Theorem Proving: After 25 Years","author":"L. Wos","year":"1984","unstructured":"L. Wos and S. Winker. Open questions solved with the assistance of AURA. In W. Bledsoe and D. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 5\u201348. American Mathematical Society, Providence, RI, 1984."},{"key":"14_CR29","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"Larry Wos. Automated Reasoning: 33 Basic Research Problems. Prentice Hall, Englewood Cliffs, NJ, 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:33Z","timestamp":1605647853000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}