{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183804},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_200","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:21:38Z","timestamp":1330251698000},"page":"668-672","source":"Crossref","is-referenced-by-count":3,"title":["A natural deduction automated theorem proving system"],"prefix":"10.1007","author":[{"given":"Li","family":"Dafa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"50_CR1","volume-title":"An Introduction To Mathematical Logic And Type Theory: To Truth Trough Proof","author":"P.B. Andrews","year":"1986","unstructured":"Andrews, P.B., An Introduction To Mathematical Logic And Type Theory: To Truth Trough Proof, Orlando, Academic Pr., Inc., 1986."},{"doi-asserted-by":"crossref","unstructured":"Andrews, P.B., Transforming Mating Into Natural Deduction Proofs. 5th Conference On Automated Deduction, Les Arcs, Prance, edited by G.Goos and J. Hartmanis, Lecture Notes in Computer Science 138, Spring-Verlag, July 8\u201311,1980.","key":"50_CR2","DOI":"10.1007\/3-540-10009-1_22"},{"key":"50_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W., Non-resolution theorem proving, Artificial Intelligence 9 (1977) 1\u201335.","journal-title":"Artificial Intelligence"},{"key":"50_CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.L. Chang","year":"1973","unstructured":"Chang, C.L. and Lee, R.C.T., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"unstructured":"Dan Sahlin, Torkel Franzen and Seif Haridi, An Intuitionistic Predicate Logic Theorem Prover. SICS Research Report R89001, ISSN 0283-3638. Swedish Institute Of Computer Science.","key":"50_CR5"},{"key":"50_CR6","first-page":"68","volume-title":"Investications into Logical Deductions. The Collected Papres of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G. Investications into Logical Deductions. The Collected Papres of Gerhard Gentzen, M.E. Szabo, ED., North-Holland Publishing CO., Amsterdam, 1969, pp. 68\u2013131."},{"unstructured":"Li Dafa, Unification Algorithm with Quantifiers in the First-Order Logic, Science Report 89005, Dept. of Applied Mathematics of Tsinghua University, Nov. 1989.","key":"50_CR7"},{"key":"50_CR8","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z. Mathematical Theory of Computation, McGraw Hill, New york, 1974."},{"key":"50_CR9","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0004-3702(89)90035-0","volume":"38","author":"D. Pastre","year":"1989","unstructured":"Pastre, Dominigue, MUS(ADET: An Automatic Theorem Proving System Using Knowledge and Metaknowledge in Mathematics, Artificial Intelligence 38 (1989) 257\u2013318.","journal-title":"Artificial Intelligence"},{"unstructured":"Pelletier, J., Further Developments in THINKER, an Automated Theorem prover: Technical Report TR-ARP-16\/87, Dept. of Computer Science, University of Alberta, CANADA.","key":"50_CR10"},{"key":"50_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"J. Pelletier","year":"1986","unstructured":"Pelletier, J., Seventy-Five Problems for Testing Automatic Theorem Provers, J. of Automated Reasoning 2 (1986) 191\u2013216.","journal-title":"J. of Automated Reasoning"},{"issue":"1","key":"50_CR12","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A., A Machine-orienteal Logic Based on the Resolution Principle, JACM, 12, 1 (Jan. 1965), 23\u201341.","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_200.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:00:25Z","timestamp":1605646825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_200","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}