{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:25Z","timestamp":1725490225508},"publisher-location":"Berlin, Heidelberg","reference-count":55,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745648"},{"type":"electronic","value":"9783540745655"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74565-5_2","type":"book-chapter","created":{"date-parts":[[2007,8,25]],"date-time":"2007-08-25T02:01:04Z","timestamp":1188007264000},"page":"2-18","source":"Crossref","is-referenced-by-count":2,"title":["Early History and Perspectives of Automated Deduction"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Bibel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. Journal of the ACM\u00a028, 193\u2013214 (1981)","journal-title":"Journal of the ACM"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Antonsen, R., Waaler, A.: Liberalized variable splitting. J. Automated Reasoning (2007)","DOI":"10.1007\/s10817-006-9055-9"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/256303.256313","volume":"44","author":"W. Bibel","year":"1997","unstructured":"Bibel, W., Eder, E.: Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution. Journal of the ACM\u00a044(2), 320\u2013344 (1997)","journal-title":"Journal of the ACM"},{"issue":"13","key":"2_CR4","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"Beth, E.W.: Semantic entailment and formal derivability. Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen\u00a018(13), 309\u2013342 (1955)","journal-title":"Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen"},{"key":"2_CR5","unstructured":"Beth, E.W.: On machines which prove theorems. Simon Stevin Wis- en Naturkundig Tijdschrift\u00a032, 49\u201360, Reprinted in [SW83, 76\u201390] (1958)"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices. Comm.\u00a0ACM\u00a026, 844\u2013852 (1983)","journal-title":"Comm.\u00a0ACM"},{"key":"2_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Vieweg Verlag, Braunschweig (1987)","edition":"2"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Lehren vom Leben \u2013 Essays \u00fcber Mensch und Gesellschaft. In: Sozialwissenschaft, Deutscher Universit\u00e4ts-Verlag, Wiesbaden (2003)","DOI":"10.1007\/978-3-322-81292-6"},{"key":"2_CR9","unstructured":"Bibel, W.: Transition logic revisited, 2004 (submitted)"},{"key":"2_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/11829263_2","volume-title":"Reasoning, Action and Interaction in AI Theories and Systems","author":"W. Bibel","year":"2006","unstructured":"Bibel, W.: Research perspectives for logic and deduction. In: Stock, O., Schaerf, M. (eds.) Reasoning, Action and Interaction in AI Theories and Systems. LNCS (LNAI), vol.\u00a04155, pp. 25\u201343. Springer, Heidelberg (2006)"},{"key":"2_CR11","unstructured":"Bibel, W.: Wissenssysteme und Komplexit\u00e4tsbew\u00e4ltigung. In: Leiber, T. (ed.) Denken und Handeln in einer komplexen Welt \u2013 Festschrift zum 60. Geburtstag von Professor Klaus Mainzer, Hirzel Verlag, Stuttgart (2007)"},{"key":"2_CR12","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, Illinois (1937)"},{"key":"2_CR13","unstructured":"Br\u00fcning, W.: Grundlagen der Strengen Logik. K\u00f6nigshausen und Neumann, W\u00fcrzburg (1996)"},{"key":"2_CR14","first-page":"281","volume":"3","author":"R. Cordeschi","year":"1996","unstructured":"Cordeschi, R.: The role of heuristics in automated theorem proving \u2013 J.A. Robinson\u2019s resolution principle. Mathware & Soft Computing\u00a03, 281\u2013293 (1996)","journal-title":"Mathware & Soft Computing"},{"key":"2_CR15","unstructured":"Davis, M.: A computer program for Presburger\u2019s algorithm. In: Summaries of talks presented at the Summer Institute for Symbolic Logic, Princeton NJ, pp. 215\u2013233, Institute for Defense Analysis (1957), Also contained in [SW83, 41\u201348]"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Davis, M.: Eliminating the irrelevant from mechanical proofs. In: Proc. Symposium for Applied Mathematics XV, Providence, RI, pp. 15\u201330 (1963), Also contained in [SW83, 315\u2013330]","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"2_CR17","first-page":"1","volume-title":"Automation of Reasoning 1 \u2013 Classical Papers on Computational Logic 1957\u20131966","author":"M. Davis","year":"1983","unstructured":"Davis, M.: The Prehistory and Early History of Automated Deduction. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1 \u2013 Classical Papers on Computational Logic 1957\u20131966, pp. 1\u201328. Springer, Berlin (1983)"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Dunham, B., Fridshal, R., Sward, G.L.: A non-heuristic program for proving elementary logical theorems. In: First International Conference on Information Processing, Paris, pp. 282\u2013285. Unesco House (1960), Also contained in [SW83, 93\u201398]","DOI":"10.1007\/978-3-642-81952-0_7"},{"key":"2_CR19","unstructured":"Dunham, B., North, J.H.: Theorem testing by computer. In: Proc. Sympos, Brooklyn NY, pp. 173\u2013177. Polytechnic Press (1963) Also contained in [SW83, 271\u2013275]"},{"key":"2_CR20","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of ACM\u00a07, 201\u2013215 (1960), Also contained in [SW83, 125\u2013139]","journal-title":"Journal of ACM"},{"key":"2_CR21","volume-title":"Completeness, Confluence, and Related Properties of Clause Graph Resolution","author":"N. Eisinger","year":"1991","unstructured":"Eisinger, N.: Completeness, Confluence, and Related Properties of Clause Graph Resolution. Pitman, London (1991)"},{"key":"2_CR22","series-title":"Synthese Library","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-94-017-0249-2_11","volume-title":"Philosophy and Logic \u2013 In search of the Polish tradition","author":"S. Feferman","year":"2003","unstructured":"Feferman, S.: Alfred tarski and a watershed meeting in logic: Cornell, 1957. In: Hintikka, J., et al. (eds.) Philosophy and Logic \u2013 In search of the Polish tradition. Synthese Library, vol.\u00a0323, pp. 151\u2013162. Kluwer Acad. Publ., Dordrecht (2003), http:\/\/math.stanford.edu\/~feferman\/papers\/cornell.pdf"},{"key":"2_CR23","unstructured":"Frege, G.: Begriffsschrift. Louis Nebert, Halle (1879)"},{"key":"2_CR24","unstructured":"Gelernter, H.: Realization of a geometry theorem-proving machine. In: Proc. First Intern. Conf. on Information Processing (IFIP), Paris, pp. 273\u2013282. UNESCO House (1959), Also contained in [SW83, 99\u2013122]"},{"key":"2_CR25","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P.C. Gilmore","year":"1960","unstructured":"Gilmore, P.C.: A proof method for quantification theory: Its justification and realization. IBM J. Research Develop.\u00a04, 28\u201335 (1960)","journal-title":"IBM J. Research Develop."},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/0004-3702(70)90005-6","volume":"1","author":"P.C. Gilmore","year":"1970","unstructured":"Gilmore, P.C.: An examination of the geometry theory machine. Artificial Intelligence\u00a01, 171\u2013187 (1970)","journal-title":"Artificial Intelligence"},{"volume-title":"J. J. Herbrand \u2014 Logical writings","year":"1971","key":"2_CR27","unstructured":"Goldfarb, W.D. (ed.): J. J. Herbrand \u2014 Logical writings. Reidel, Dordrecht (1971)"},{"key":"2_CR28","volume-title":"Grundz\u00fcge der Theoretischen Logik","author":"D. Hilbert","year":"1928","unstructured":"Hilbert, D., Ackermann, W.: Grundz\u00fcge der Theoretischen Logik. Springer, Heidelberg (1928)"},{"key":"2_CR29","unstructured":"Herbrand, J.J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. In: Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 (Mathem., Phys.) (1930), Engl. transl. in [Gol71]"},{"key":"2_CR30","first-page":"7","volume":"8","author":"K.J.J. Hintikka","year":"1955","unstructured":"Hintikka, K.J.J.: Form and content in quantification theory. Acta Philosophica Fennica\u00a08, 7\u201355 (1955)","journal-title":"Acta Philosophica Fennica"},{"issue":"1-2","key":"2_CR31","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF02279945","volume":"7","author":"G.-R. Hoffmann","year":"1971","unstructured":"Hoffmann, G.-R., Veenker, G.: The unit-clause proof procedure with equality. Computing\u00a07(1-2), 91\u2013105 (1971)","journal-title":"Computing"},{"key":"2_CR32","unstructured":"Kanger, S.: Provability in Logic. PhD thesis, University of Stockholm (1957)"},{"key":"2_CR33","volume-title":"The Development of Logic","author":"W. Kneale","year":"1984","unstructured":"Kneale, W., Kneale, M.: The Development of Logic. Clarendon Press, Oxford (1984)"},{"issue":"2","key":"2_CR34","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO \u2014 A high-performance theorem prover for first-order logic. Journal of Automated Reasoning\u00a08(2), 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR35","unstructured":"McCarthy, J.: The Wang algorithm for the propositional calculus programmed in LISP. In: McCarthy, J. (ed.) Symbol Manipulating Language Memo\u00a014, Artificial Intelligence Project, MIT, Cambridge MA (1959), Quoted in [Wan60a, p.232]"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., Wos, L.: Problems and experiments for and with automated theorem proving programs. IEEE Transactions on Computers\u00a0C-25, 773\u2013782 (1976)","journal-title":"IEEE Transactions on Computers"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Newell, A., Shaw, J.C., Simon, H.A.: The logic theory machine. IRE Trans. Information Theory\u00a0IT-2, 61\u201379 (1956), Also contained in [SW83, 49-73]","DOI":"10.1109\/TIT.1956.1056797"},{"key":"2_CR38","unstructured":"Papon, P.: Die Wissenschaft, Zeichen der Zeit. FTE Info \u2013 Magazin \u00fcber europ\u00e4ische Forschung (An interview)\u00a050, 9\u201311 (2006)"},{"key":"2_CR39","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/321021.321023","volume":"7","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D., Prawitz, H., Voghera, N.: A mechanical proof procedure and its realization in an electronic computer. J. ACM\u00a07, 102\u2013128 (1960)","journal-title":"J. ACM"},{"key":"2_CR40","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D.: An improved proof procedure. Theoria\u00a026, 102\u2013139 (1960), Also contained in [SW83, 159\u2013199]","journal-title":"Theoria"},{"key":"2_CR41","unstructured":"Robinson, A.: Proving theorems (as done by man, logician, or machine). In: Summaries of Talks Presented at the Summer Institute for Symbolic Logic, Communic. Res. Div., Princeton, New Jersey, Institute for Defense Analysis (1957), Also contained in [SW83, 74\u201376]"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Alan Robinson, J.: Gamma I: A general theorem proving program for the IBM 704. Technical Report ANL-6447, Argonne National Laboratory, Chicago, IL (1961)","DOI":"10.2172\/4808243"},{"issue":"2","key":"2_CR43","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/321160.321166","volume":"10","author":"J. Alan Robinson","year":"1963","unstructured":"Alan Robinson, J.: Theorem proving on the computer. Journ. ACM\u00a010(2), 163\u2013174 (1963), Also contained in\u00a0[SW83, 372\u2013383]","journal-title":"Journ. ACM"},{"key":"2_CR44","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Alan Robinson","year":"1965","unstructured":"Alan Robinson, J.: A machine-oriented logic based on the resolution principle. Journal of ACM\u00a012, 23\u201341 (1965), Also contained in\u00a0[SW83, 397\u2013415]","journal-title":"Journal of ACM"},{"key":"2_CR45","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-94-015-9383-0_17","volume-title":"Intellectics and Computational Logic \u2013 Papers in Honor of Wolfgang Bibel","author":"J.A. Robinson","year":"2000","unstructured":"Robinson, J.A.: PROOF=GUARANTEE+EXPLANATION. In: H\u00f6lldobler, S. (ed.) Intellectics and Computational Logic \u2013 Papers in Honor of Wolfgang Bibel. Applied Logic Series, vol.\u00a019, pp. 277\u2013294. Kluwer, Dordrecht (2000)"},{"key":"2_CR46","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/BF01969991","volume":"2","author":"K. Sch\u00fctte","year":"1956","unstructured":"Sch\u00fctte, K.: Ein System des verkn\u00fcpfenden Schlie\u00dfens. Archiv f. Mathematische Logik und Grundlagen der Wissenschaften\u00a02, 55\u201367 (1956)","journal-title":"Archiv f. Mathematische Logik und Grundlagen der Wissenschaften"},{"volume-title":"Automation of Reasoning \u2014 Classical Papers on Computational Logic 1957-1966","year":"1983","key":"2_CR47","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning \u2014 Classical Papers on Computational Logic 1957-1966, vol.\u00a01. Springer, Berlin (1983)"},{"key":"2_CR48","first-page":"127","volume":"4","author":"G. Veenker","year":"1963","unstructured":"Veenker, G.: Ein Entscheidungsverfahren f\u00fcr den Aussagenkalk\u00fcl und seine Realisation in einem Rechenautomaten. Grundl.stud. aus Kybernetik u. Geisteswiss\u00a04, 127\u2013136 (1963)","journal-title":"Grundl.stud. aus Kybernetik u. Geisteswiss"},{"issue":"3","key":"2_CR49","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BF02236612","volume":"2","author":"G. Veenker","year":"1967","unstructured":"Veenker, G.: Beweisalgorithmen f\u00fcr die Pr\u00e4dikatenlogik. Computing\u00a02(3), 263\u2013283 (1967)","journal-title":"Computing"},{"key":"2_CR50","doi-asserted-by":"publisher","first-page":"141","DOI":"10.2307\/2266900","volume":"20","author":"W. Orman Quine van","year":"1955","unstructured":"van Orman Quine, W.: A proof procedure for quantification theory. J. Symbolic Logic\u00a020, 141\u2013149 (1955)","journal-title":"J. Symbolic Logic"},{"key":"2_CR51","doi-asserted-by":"publisher","first-page":"627","DOI":"10.2307\/2307285","volume":"62","author":"W. Orman Quine van","year":"1955","unstructured":"van Orman Quine, W.: A way to simplify truth functions. American Mathematical Monthly\u00a062, 627\u2013631 (1955)","journal-title":"American Mathematical Monthly"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"Wang, H.: Proving theorems by pattern recognition, Part I. Comm.\u00a0ACM\u00a03, 220\u2013234 (1960), Also contained in\u00a0[SW83, 229\u2013243]","DOI":"10.1145\/367177.367224"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Wang, H.: Toward mechanical mathematics. IBM Journ. Res. Develop.\u00a04, 2\u201322, Also contained in\u00a0[SW83, 244\u2013264] (1960)","DOI":"10.1147\/rd.41.0002"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Wos, L., Carson, D., Robinson, G.A.: The unit preference strategy in theorem proving. In: AFIPS Conf. Proc., Washington DC, vol. 26, pp. 615\u2013621. Spartan Books (1964)","DOI":"10.1145\/1464052.1464109"},{"key":"2_CR55","first-page":"1","volume-title":"Automated Reasoning 2 \u2013 Classical Papers on Computational Logic 1967\u20131970","author":"L. Wos","year":"1983","unstructured":"Wos, L., Henschen, L.: Automated theorem proving 1965\u20131970. In: Siekmann, J., Wrightson, G. (eds.) Automated Reasoning 2 \u2013 Classical Papers on Computational Logic 1967\u20131970, vol.\u00a02, pp. 1\u201324. Springer, Berlin (1983)"}],"container-title":["Lecture Notes in Computer Science","KI 2007: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74565-5_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:24:53Z","timestamp":1619504693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74565-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745648","9783540745655"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74565-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}