{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:12:06Z","timestamp":1725455526191},"publisher-location":"Berlin\/Heidelberg","reference-count":10,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540526994"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0020872","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T05:50:56Z","timestamp":1131861056000},"page":"67-72","source":"Crossref","is-referenced-by-count":0,"title":["Intelligent CAI course in the first-order logic"],"prefix":"10.1007","author":[{"given":"Li","family":"Dafa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Andrews, P. B., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Orlando, Academic Pr., Inc., 1986."},{"key":"8_CR2","doi-asserted-by":"publisher","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\n9, 1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"key":"8_CR3","unstructured":"Dafa, Li, Extended Tautology, Journal of Tsinghua University, Vol. 27, No.3, 1987."},{"key":"8_CR4","unstructured":"Manna, Z., Mathematical Theory of Computation, New York, 1974."},{"issue":"2","key":"8_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J., Seventy-Five problems for Testing Automatic Theorem provers, J. of Automated Reasoning, Vol.\n2, No. 2, 191\u2013216, 1986.","journal-title":"J. of Automated Reasoning"},{"key":"8_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"Smullyan, R. M., First-Order Logic, Springer-Verlag, New York, 1968."},{"key":"8_CR7","volume-title":"Discrete Mathematics in Computer Science","author":"D. F. Stanat","year":"1977","unstructured":"Stanat, D. F. and McAlliister, D. F., Discrete Mathematics in Computer Science, Prentice-Hall, Inc., Englewood Cliffs, N.J., 1977."},{"key":"8_CR8","unstructured":"Suppes Patrick, University-Level Computer-Asisted Instrution At Stanford: 1968\u20131980."},{"key":"8_CR9","volume-title":"Discrete Mathematial Structures with Applications to Computer Science","author":"J. P. Tremblay","year":"1975","unstructured":"Tremblay, J. P. and Manohar, R., Discrete Mathematial Structures with Applications to Computer Science, New York, McGray-Hill, 1975."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Wos, L., Automated Reasoning, American Mathematical Monthly, Vol.\n92,No.2, Feb. 1985.","DOI":"10.1080\/00029890.1985.11971545"}],"container-title":["Lecture Notes in Computer Science","Computer Assisted Learning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0020872.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:45:27Z","timestamp":1607550327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0020872"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540526994"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0020872","relation":{},"subject":[]}}