{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T11:19:49Z","timestamp":1648639189914},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1988,4,1]],"date-time":"1988-04-01T00:00:00Z","timestamp":575856000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AI & Soc"],"published-print":{"date-parts":[[1988,4]]},"DOI":"10.1007\/bf01891376","type":"journal-article","created":{"date-parts":[[2005,7,5]],"date-time":"2005-07-05T13:22:05Z","timestamp":1120569725000},"page":"121-131","source":"Crossref","is-referenced-by-count":0,"title":["Human-oriented and machine-oriented reasoning: Remarks on some problems in the history of Automated Theorem Proving"],"prefix":"10.1007","volume":"2","author":[{"given":"Furio","family":"Di Paola","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF01891376_CR1","volume-title":"Scienza e Filosofia","author":"C. Bernardi","year":"1985","unstructured":"Bernardi, C. and P. Pagli (1985) Modelli naturali, assiomatizzazione, incompletezza, in C. Mangione (ed.)Scienza e Filosofia. Garzanti, Milan."},{"key":"BF01891376_CR2","unstructured":"Bledsoe, W.W. (1979). Non-resolution Theorem Proving,Artificial Intelligence. 9."},{"key":"BF01891376_CR3","unstructured":"Bledsoe, W.W. and P. Bruell (1973). A Man-machine Theorem Proving System. Rep. TEX 39, Dept. of AI, Edinburgh."},{"key":"BF01891376_CR4","unstructured":"Bledsoe, W.W. and D.W. Loveland (eds) (1983). Automated Theorem Proving: After 25 Years.Contemporary Mathematics. 29. AMS, Providence-Rhode Island."},{"key":"BF01891376_CR5","doi-asserted-by":"crossref","unstructured":"Boyer, R.S. and J.S. Moore (1983). Proof-Checking, Theorem Proving and Program Verification, in [4].","DOI":"10.1090\/conm\/029\/07"},{"key":"BF01891376_CR6","volume-title":"Machine Intelligence 10","author":"K.A. Bowen","year":"1982","unstructured":"Bowen, K.A. (1982) Programming with Full First-order Logic, in Hayes-Michie-Pao (eds)Machine Intelligence 10. Ellis Horwood, Chichester."},{"key":"BF01891376_CR7","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"A. Bundy","year":"1983","unstructured":"Bundy, A. (1983).The Computer Modelling of Mathematical Reasoning. Academic Press, London."},{"key":"BF01891376_CR8","volume-title":"Proceedings of the 9th IJCAI","author":"A. Bundy","year":"1985","unstructured":"Bundy, A. (1985). Discovery and Reasoning in Mathematics.Proceedings of the 9th IJCAI. Morgan Kaufman, Los Altos."},{"key":"BF01891376_CR9","doi-asserted-by":"crossref","unstructured":"Cellucci, C. (1985). Proof Theory and Complexity.Synthese. 62.","DOI":"10.1007\/BF00486045"},{"key":"BF01891376_CR10","unstructured":"Cellucci, C. (1986). Using Full First-order Logic as a Programming Language, workshopLogic and Computer Science: New Trends and Applications. Turin."},{"key":"BF01891376_CR11","unstructured":"Cellucci, C. (1987). La Logica e l'intelligenza artificiale, in Riuniti (ed.)Ulisse. Rome."},{"key":"BF01891376_CR12","doi-asserted-by":"crossref","unstructured":"Davis, M. (1983). The Prehistory and Early History of Automated Deduction, in [25], 1.","DOI":"10.1007\/978-3-642-81952-0_1"},{"key":"BF01891376_CR13","volume-title":"Studi sociali della scienza","author":"F. Paola Di","year":"1988","unstructured":"Di Paola, F. (1988). Matematici, computer-assisted proof e teorema dei quattro colori, forthcoming in Cannar\u00f2 (ed.)Studi sociali della scienza. Angeli, Milan."},{"key":"BF01891376_CR14","doi-asserted-by":"crossref","unstructured":"Feigenbaum, E.A. (1984). Knowledge Engineering: The Applied Side, in [18].","DOI":"10.1111\/j.1749-6632.1984.tb16513.x"},{"key":"BF01891376_CR15","volume-title":"Logical Foundations of Artificial Intelligence","author":"M.R. Genesereth","year":"1987","unstructured":"Genesereth, M.R. and N.J. Nilsson (1987).Logical Foundations of Artificial Intelligence. Kaufmann, Los Altos."},{"key":"BF01891376_CR16","volume-title":"Logica, Studia Paul Bernays Dedicata","author":"K. G\u00f6del","year":"1959","unstructured":"G\u00f6del, K. (1959). Uber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunktes.Logica, Studia Paul Bernays Dedicata. Griffon, Neuch\u00e2tel."},{"key":"BF01891376_CR17","volume-title":"Methods of Heuristics","year":"1983","unstructured":"Groner, M., R. Groner and W.F. Bischof (eds) (1983).Methods of Heuristics. Erlbaum, Hillsdale, New Jersey."},{"key":"BF01891376_CR18","volume-title":"Intelligent Systems: The Unprecedented Opportunity","year":"1984","unstructured":"Hayes, J.E. and D. Michie (eds) (1984).Intelligent Systems: The Unprecedented Opportunity. Ellis Horwood, Chichester."},{"key":"BF01891376_CR19","unstructured":"Kreisel, G. (1977). On the Kind of Data Needed for a Theory of Proofs, in Barwise et al. (eds)Logic Colloquium. Amsterdam."},{"key":"BF01891376_CR20","unstructured":"Kreisel, G. (1970). Hilbert's Programme and the Search for Automatic Proof Procedures, inSymposium on Automatic Demonstration, Lecture Notes in Mathematics. Springer."},{"key":"BF01891376_CR21","unstructured":"Loveland, D.W. (1983). (1983). Automated Theorem Proving: A Quarter Century Review, in [4]."},{"key":"BF01891376_CR22","unstructured":"Reichgel, T.H. (1987). A Review of McDermott'sCritique of Pure Reason. InAI Communications. 1."},{"key":"BF01891376_CR23","unstructured":"Robinson, J.A. (1984). Logical Reasoning in Machines, in [18]."},{"key":"BF01891376_CR24","unstructured":"Shepherdson, J.C. (1984). The Calculus of Reasoning, in [18]."},{"key":"BF01891376_CR25","volume-title":"Automation of Reasoning, 1\u20132","year":"1983","unstructured":"Siekmann, J. and B. Wrightson (eds) (1983).Automation of Reasoning, 1\u20132. Springer, Berlin."},{"key":"BF01891376_CR26","doi-asserted-by":"crossref","unstructured":"Wang, H. (1960). Towards Mechanical Mathematics.IBM Journal of Research and Development. 4.","DOI":"10.1147\/rd.41.0002"},{"key":"BF01891376_CR27","volume-title":"Popular Lectures on Mathematical Logic","author":"H. Wang","year":"1981","unstructured":"Wang, H. (1981).Popular Lectures on Mathematical Logic. Van Nostrand, New York."},{"key":"BF01891376_CR28","doi-asserted-by":"crossref","unstructured":"Wang, H. (1983). Computer Theorem Proving and Artificial Intelligence, in [4].","DOI":"10.1090\/conm\/029\/749239"},{"key":"BF01891376_CR29","volume-title":"Mathematics as a Cultural System","author":"R. Wilder","year":"1981","unstructured":"Wilder, R. (1981).Mathematics as a Cultural System. Pergamon, Oxford."},{"key":"BF01891376_CR30","doi-asserted-by":"crossref","unstructured":"Wos. L. and L. Henschen (1983). Automated Theorem Proving 1965\u20131970, in [25], 2.","DOI":"10.1007\/978-3-642-81955-1_1"},{"key":"BF01891376_CR31","doi-asserted-by":"crossref","unstructured":"Wos, L. (1987). Some Obstacles to the Automation of Reasoning, and the Problem of Redundant Information.Journal of Automated Reasoning. 3.","DOI":"10.1007\/BF00381146"}],"container-title":["AI & SOCIETY"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01891376.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01891376\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01891376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T04:27:54Z","timestamp":1586320074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01891376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,4]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1988,4]]}},"alternative-id":["BF01891376"],"URL":"https:\/\/doi.org\/10.1007\/bf01891376","relation":{},"ISSN":["0951-5666","1435-5655"],"issn-type":[{"value":"0951-5666","type":"print"},{"value":"1435-5655","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988,4]]}}}