{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:11Z","timestamp":1755220931589,"version":"3.43.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[1998,1]]},"DOI":"10.1023\/a:1005035316026","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T15:31:12Z","timestamp":1040484672000},"page":"3-43","source":"Crossref","is-referenced-by-count":9,"title":["Automated Natural Deduction in Thinker"],"prefix":"10.1007","volume":"60","author":[{"given":"Francis Jeffry","family":"Pelletier","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"155398_CR1","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00243811","volume":"7","author":"P. Andrews","year":"1991","unstructured":"Andrews, P. (1991), 'More on the problem of finding a mapping between clause representation and natural-deduction representation', Journal of Automated Reasoning 7, 285-286.","journal-title":"Journal of Automated Reasoning"},{"key":"155398_CR2","volume-title":"The Logic Book","author":"M. Bergmann","year":"1990","unstructured":"Bergmann, M., J. Moor, J. Nelson (1990), The Logic Book, 2nd Ed, NY: McGraw-Hill.","edition":"2nd Ed"},{"key":"155398_CR3","doi-asserted-by":"crossref","unstructured":"Beth, F. (1958), 'On machines which prove theorems', in Siekmann & Wrightson, 79-90.","DOI":"10.1007\/978-3-642-81952-0_6"},{"key":"155398_CR4","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0004-3702(71)90004-X","volume":"2","author":"W. Bledsoe","year":"1971","unstructured":"Bledsoe, W. (1971), 'Splitting and reduction heuristics in automatic theorem proving', Artificial Intelligence 2, 55-78.","journal-title":"Artificial Intelligence"},{"key":"155398_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. Bledsoe","year":"1977","unstructured":"Bledsoe, W. (1977), 'Non-resolution theorem proving', Artificial Intelligence 9, 1-35.","journal-title":"Artificial Intelligence"},{"key":"155398_CR6","unstructured":"Bledsoe, W. (1983), The UT Natural-Deduction Prover, Technical Report, Dept. Computer Science, Univ. Texas."},{"key":"155398_CR7","first-page":"269","volume-title":"Proceedings of PACLING","author":"A. Edgar","year":"1993","unstructured":"Edgar, A. & F. J. Pelletier (1993), 'Natural language generation from natural deduction proofs', Proceedings of PACLING, Vancouver: Simon Fraser Univ., 269-278."},{"key":"155398_CR8","volume-title":"The Logic Course","author":"S. De Haven","year":"1994","unstructured":"De Haven, S. (1994), The Logic Course, Pigeon Enterprises: Calgary."},{"key":"155398_CR9","doi-asserted-by":"crossref","unstructured":"Kalish, D. (1974), 'Review of I. Copi Symbolic Logic', Journal of Symbolic Logic, 177-178.","DOI":"10.2307\/2272366"},{"key":"155398_CR10","volume-title":"Logic","author":"D. Kalish","year":"1964","unstructured":"Kalish, D. & R. Montague (1964), Logic, Hartcourt, Brace, Janovich."},{"key":"155398_CR11","volume-title":"Logic","author":"D. Kalish","year":"1980","unstructured":"Kalish, D., R. Montague, and G. Mar (1980), Logic, Hartcourt, Brace, Janovich."},{"key":"155398_CR12","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1023\/A:1005749401809","volume":"18","author":"D. Li","year":"1997","unstructured":"Li Dafa (1997), 'Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving', Journal of Automated Reasoning 18, 105-134.","journal-title":"Journal of Automated Reasoning"},{"key":"155398_CR13","doi-asserted-by":"crossref","unstructured":"Newell, A., J. Shaw, H. Simon (1957), 'Empirical explorations with the logic theory machine', in Siekmann & Wrightson, 49-73.","DOI":"10.1007\/978-3-642-81952-0_4"},{"key":"155398_CR14","unstructured":"Pelletier, F. J. (1982), Completely Non-Clausal, Completely Heuristic-Driven, Automatic Theorem Proving, Tech. Report TR82-7, Dept. Computing Science, Univ. Alberta."},{"key":"155398_CR15","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"3","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J. (1986\/7), '75 graduated problems for testing automated theorem provers', Journal of Automated Reasoning 3, 191-216, and 'Errata for 75 problems', Journal of Automated Reasoning 4, 235\u2013236.","journal-title":"Journal of Automated Reasoning"},{"key":"155398_CR16","unstructured":"Pelletier, F. J. (1987), Further Developments in THINKER, an Automated Theorem Prover, Tech. Report TR-ARP-16\/87 Automated Reasoning Project, Australia National University."},{"key":"155398_CR17","unstructured":"Pelletier, F. J. (1991), 'The philosophy of automated theorem proving', Proceedings of IJCAI-91, Morgan Kaufmann, 1039-1045."},{"key":"155398_CR18","unstructured":"Pelletier, F. J. (1993a), 'Automated modal logic theorem proving in Thinker', Technical Report TR 93-14, Dept. Computing Science, Univ. Alberta."},{"key":"155398_CR19","doi-asserted-by":"crossref","unstructured":"Pelletier, F. J. (1993b), 'Identity in modal logic theorem proving', Studia Logica 52, 291-308.","DOI":"10.1007\/BF01058393"},{"key":"155398_CR20","first-page":"4","volume":"6","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J. & P. Rudnicki (1986), 'Non-obviousness', Newsletter of the Association for Automated Reasoning, No. 6, 4-6.","journal-title":"Newsletter of the Association for Automated Reasoning"},{"key":"155398_CR21","first-page":"419","volume":"6","author":"J. Pollock","year":"1992","unstructured":"Pollock, J. (1992a), 'Interest-driven suppositional reasoning', Journal of Automated Reasoning 6, 419-462.","journal-title":"Journal of Automated Reasoning"},{"key":"155398_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(92)90103-5","volume":"57","author":"J. Pollock","year":"1992","unstructured":"Pollock, J. (1992b), 'How to reason defeasibly', Artificial Intelligence 57, 1-42.","journal-title":"Artificial Intelligence"},{"key":"155398_CR23","unstructured":"Pollock, J. (1997), 'Skolemization and unification in natural deduction', unpublished paper available at http:\/\/www.u.arizona.edu\/~pollock\/."},{"key":"155398_CR24","volume-title":"Logic with SYMLOG","author":"F. Portoraro","year":"1994","unstructured":"Portoraro, F. & R. Tully (1994), Logic with SYMLOG, Prentice Hall: Englewood Cliffs."},{"key":"155398_CR25","doi-asserted-by":"crossref","unstructured":"Prawitz, D., H. Prawitz & N. Voghera (1960), 'A mechanical proof procedure and its realization in an electronic computer' in Siekmann & Wrightson, 202-228.","DOI":"10.1007\/978-3-642-81952-0_13"},{"key":"155398_CR26","unstructured":"Sieg, W. & J. Byrnes (1996), 'Normal natural deduction proofs (in classical logic)', Technical Report PHIL-74, Dept. Philosophy, Carnegie Mellon Univ."},{"key":"155398_CR27","unstructured":"Sieg, W. & B. Kauffmann (1993), 'Unification for quantified formulae', Technical Report PHIL-46, Dept. Philosophy, Carnegie Mellon Univ."},{"key":"155398_CR28","first-page":"137","volume-title":"Philosophy and the Computer","author":"W. Sieg","year":"1992","unstructured":"Sieg, W. & R. Scheines (1992), 'Searching for proofs (in sentential logic)', in L. Burkholder (ed.), Philosophy and the Computer, Westview: Boulder, 137-159."},{"key":"155398_CR29","doi-asserted-by":"crossref","unstructured":"Siekmann, J. & G. Wrightson (1983), The Automation of Reasoning, Vol. 1, Springer-Verlag.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"155398_CR30","doi-asserted-by":"crossref","unstructured":"Smullyan, R. (1968), First Order Logic, Springer-Verlag.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"155398_CR31","unstructured":"Suppes, P. (1981), University-Level Computer-Assisted Instruction at Stanford, 1968\u20131981, Institute for Mathematical Studies in the Social Sciences: Stanford Univ."},{"key":"155398_CR32","doi-asserted-by":"crossref","unstructured":"Wang, H. (1960), 'Toward mechanical mathematics', reprinted in Siekmann & Wrightson 1983, 244\u2013264.","DOI":"10.1007\/978-3-642-81952-0_15"},{"key":"155398_CR33","unstructured":"Whitehead, A. & B. Russell (1910), Principia Mathematica, Vol. I. Cambridge Univ. Press."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005035316026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005035316026\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005035316026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:16:17Z","timestamp":1754630177000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005035316026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,1]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,1]]}},"alternative-id":["155398"],"URL":"https:\/\/doi.org\/10.1023\/a:1005035316026","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1998,1]]}}}