{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:21Z","timestamp":1725542961941},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540370338"},{"type":"electronic","value":"9783540370352"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11811220_43","type":"book-chapter","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T12:40:48Z","timestamp":1153744848000},"page":"514-524","source":"Crossref","is-referenced-by-count":2,"title":["An Extension Rule Based First-Order Theorem Prover"],"prefix":"10.1007","author":[{"given":"Xia","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jigui","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kun","family":"Hou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"43_CR1","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1023\/A:1027339205632","volume":"31","author":"H. Lin","year":"2003","unstructured":"Lin, H., Sun, J.G., Zhang, Y.M.: Theorem proving based on extension rule. Journal of Automated Reasoning\u00a031, 11\u201321 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"43_CR2","first-page":"190","volume":"6","author":"X. Wu","year":"2006","unstructured":"Wu, X., Sun, J.G., Lu, S., Yin, M.H.: Propositional extension rule with reduction. International Journal of Computer Science and Network Security\u00a06, 190\u2013195 (2006)","journal-title":"International Journal of Computer Science and Network Security"},{"key":"43_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/11795131_86","volume-title":"Rough Sets and Knowledge Technology","author":"X. Wu","year":"2006","unstructured":"Wu, X., Sun, J.G., Lu, S., Li, Y., Meng, W.: Improved propositional extension rule. In: Wang, G.-Y., Peters, J.F., Skowron, A., Yao, Y. (eds.) RSKT 2006. LNCS, vol.\u00a04062, pp. 592\u2013597. Springer, Heidelberg (2006)"},{"key":"43_CR4","doi-asserted-by":"crossref","unstructured":"Wu, X., Sun, J.G., Hou, K.: Extension rule in first order logic. In: Proceeding of 5th International Conference on Cognitive Informatics (ICCI 2006), Beijing, China (to appear, 2006)","DOI":"10.1109\/COGINF.2006.365574"},{"key":"43_CR5","doi-asserted-by":"crossref","unstructured":"Chu, H., Plaisted, D.A.: Semantically Guided First-Order Theorem Proving Using Hyper-Linking. In: Proceeding of 12th Conference on Automated Deduction, Nancy, France, pp. 192\u2013206 (1994)","DOI":"10.1007\/3-540-58156-1_14"},{"key":"43_CR6","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1023\/A:1005847700447","volume":"18","author":"M. Paramasivam","year":"1997","unstructured":"Paramasivam, M., Plaisted, A.D.: A replacement rule theorem prover. Journal of Automated Reasoning\u00a018, 221\u2013226 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"43_CR7","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0167-9236(88)90128-5","volume":"4","author":"R.G. Jeroslow","year":"1988","unstructured":"Jeroslow, R.G.: Computation-oriented reductions of predicate to propositional logic. Decision Support Systems\u00a04, 183\u2013197 (1988)","journal-title":"Decision Support Systems"},{"key":"43_CR8","volume-title":"Symbolic logic and mechanical theorem proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., Lee, R.C.: Symbolic logic and mechanical theorem proving. Academic Press, London (1973)"},{"key":"43_CR9","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Proceeding of the 10th European Conference on Artificial Intelligence, Vienna, Austria, pp. 359\u2013363 (1992)"},{"key":"43_CR10","unstructured":"Wu, X., Sun, J.G., Feng, S.S.: Destructive extension rule in modal logic K. In: Proceeding of International Conference of Computational Methods, Singapore (2004)"},{"key":"43_CR11","first-page":"550","volume":"6","author":"X. Wu","year":"2005","unstructured":"Wu, X., Sun, J.G., Lin, H., Feng, S.S.: Modal extension rule. Process In Natural Science, China\u00a06, 550\u2013558 (2005)","journal-title":"Process In Natural Science, China"}],"container-title":["Lecture Notes in Computer Science","Knowledge Science, Engineering and Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11811220_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:26:50Z","timestamp":1619508410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11811220_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540370338","9783540370352"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11811220_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}