{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T04:41:05Z","timestamp":1769575265744,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":111,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540734321","type":"print"},{"value":"9783540734338","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73433-8_24","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T14:36:40Z","timestamp":1186843000000},"page":"334-349","source":"Crossref","is-referenced-by-count":6,"title":["A Short Survey of Automated Reasoning"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning\u00a016, 321\u2013353 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K. Appel","year":"1976","unstructured":"Appel, K., Haken, W.: Every planar map is four colorable. Bulletin of the American Mathematical Society\u00a082, 711\u2013712 (1976)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"24_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"24_CR4","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures Rewriting Techniques","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures Rewriting Techniques, vol.\u00a02, pp. 1\u201330. Academic Press, San Diego (1989)"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of EuroSys 2006, the European Systems Conference (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"24_CR6","volume-title":"Philosophy of mathematics: selected readings","author":"P. Benacerraf","year":"1983","unstructured":"Benacerraf, P., Putnam, H.: Philosophy of mathematics: selected readings, 2nd edn. Cambridge University Press, Cambridge (1983)","edition":"2"},{"key":"24_CR7","first-page":"309","volume":"18","author":"E.W. Beth","year":"1955","unstructured":"Beth, E.W.: Semantic entailment and formal derivability. Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, new series\u00a018, 309\u2013342 (1955)","journal-title":"Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen, new series"},{"key":"24_CR8","first-page":"1736","volume-title":"Graph Theory","author":"N.L. Biggs","year":"1976","unstructured":"Biggs, N.L., Lloyd, E.K., Wilson, R.J.: Graph Theory, pp. 1736\u20131936. Clarendon Press, Oxford (1976)"},{"key":"24_CR9","series-title":"International Series in Engineering and Computer Science","volume-title":"VLSI Specification, Verification and Synthesis","year":"1988","unstructured":"Birtwistle, G., Subrahmanyam, P.A. (eds.): VLSI Specification, Verification and Synthesis. International Series in Engineering and Computer Science, vol.\u00a035. Kluwer, Dordrecht (1988)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Bledsoe, W.W.: Some automatic proofs in analysis. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years, Contemporary Mathematics, vol. 29, pp. 89\u2013118. American Mathematical Society (1984)","DOI":"10.1090\/conm\/029\/06"},{"key":"24_CR11","first-page":"183","volume":"3","author":"G. Boole","year":"1848","unstructured":"Boole, G.: The calculus of logic. The Cambridge and Dublin Mathematical Journal\u00a03, 183\u2013198 (1848)","journal-title":"The Cambridge and Dublin Mathematical Journal"},{"key":"24_CR12","volume-title":"Elements of mathematics Translated from French Th\u00e9orie des ensembles in the series El\u00e9ments de math\u00e9matique , originally published by Hermann","author":"N. Bourbaki","year":"1968","unstructured":"Bourbaki, N.: Theory of sets. In: Elements of mathematics Translated from French Th\u00e9orie des ensembles in the series El\u00e9ments de math\u00e9matique, originally published by Hermann, Addison-Wesley, London (1968)"},{"key":"24_CR13","series-title":"ACM Monograph Series","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monograph Series. Academic Press, San Diego (1979)"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/103516.103519","volume":"38","author":"R.E. Bryant","year":"1991","unstructured":"Bryant, R.E.: A method for hardware verification based on logic simulation. Journal of the ACM\u00a038, 299\u2013328 (1991)","journal-title":"Journal of the ACM"},{"key":"24_CR16","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Mathematisches Institut der Universit\u00e4t Innsbruck, 1965. English translation to appear in Journal of Symbolic Computation (2006)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Buchberger, B.: Ein algorithmisches Kriterium fur die L\u00f6sbarkeit eines algebraischen Gleichungssystems. Aequationes Mathematicae, vol. 4, 374\u2013383, 1970, English translation An Algorithmical Criterion for the Solvability of Algebraic Systems of Equations in [18] pp. 535\u2013545 (1970)","DOI":"10.1007\/BF01844169"},{"key":"24_CR18","series-title":"London Mathematical Society Lecture Note Series","volume-title":"Gr\u00f6bner Bases and Applications","year":"1998","unstructured":"Buchberger, B., Winkler, F. (eds.): Gr\u00f6bner Bases and Applications. London Mathematical Society Lecture Note Series, vol.\u00a0251. Cambridge University Press, Cambridge (1998)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Bumcrot, R.: On lattice complements. In: Proceedings of the Glasgow Mathematical Association\u00a07, 22\u201323 (1965)","DOI":"10.1017\/S2040618500035103"},{"key":"24_CR20","first-page":"178","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"A. Bundy","year":"1991","unstructured":"Bundy, A.: A science of reasoning. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178\u2013198. MIT Press, Cambridge (1991)"},{"key":"24_CR21","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and monographs in symbolic computation","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and monographs in symbolic computation. Springer, Heidelberg (1998)"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00244942","volume":"4","author":"S.-C. Chou","year":"1988","unstructured":"Chou, S.-C.: An introduction to Wu\u2019s method for mechanical theorem proving in geometry. Journal of Automated Reasoning\u00a04, 237\u2013267 (1988)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR23","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A. Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number-theory. American Journal of Mathematics\u00a058, 345\u2013363 (1936)","journal-title":"American Journal of Mathematics"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"24_CR25","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Cohn, A.: A proof of correctness of the VIPER microprocessor: The first level. In: Birtwistle and Subrahmanyam [9], pp. 27\u201371","DOI":"10.1007\/978-1-4613-2007-4_2"},{"issue":"3","key":"24_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/141897.141901","volume":"26","author":"R.M. Corless","year":"1992","unstructured":"Corless, R.M., Jeffrey, D.J.: Well... it isn\u2019t quite that simple. SIGSAM Bulletin\u00a026(3), 2\u20136 (1992)","journal-title":"SIGSAM Bulletin"},{"issue":"2","key":"24_CR28","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/235699.235705","volume":"30","author":"R.M. Corless","year":"1996","unstructured":"Corless, R.M., Jeffrey, D.J.: The unwinding number. SIGSAM Bulletin\u00a030(2), 28\u201335 (1996)","journal-title":"SIGSAM Bulletin"},{"key":"24_CR29","unstructured":"Davis, M.: A computer program for Presburger\u2019s algorithm. In: Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell University, pp. 215\u2013233. Institute for Defense Analyses, Princeton, NJ, Reprinted in [94], pp. 41\u201348 (1957)"},{"key":"24_CR30","volume-title":"The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions","year":"1965","unstructured":"Davis, M. (ed.): The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Raven Press, NY (1965)"},{"key":"24_CR31","doi-asserted-by":"publisher","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 the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: The mathematical language AUTOMATH, its usage and some of its extensions. In: Laudet, et al. [67], pp. 29\u201361","DOI":"10.1007\/BFb0060623"},{"key":"24_CR33","first-page":"589","volume-title":"To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project AUTOMATH. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 589\u2013606. Academic Press, San Diego (1980)"},{"key":"24_CR34","unstructured":"de Nivelle, H.: Ordering Refinements of Resolution. PhD thesis, Technische Universiteit Delft (1995)"},{"key":"24_CR35","first-page":"205","volume-title":"Selected Writings on Computing: A Personal Perspective Paper prepared for Symposium on the Mathematical Foundations of Computing Science","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: Formal techniques and sizeable programs (EWD563). In: Dijkstra, E.W. (ed.) Selected Writings on Computing: A Personal Perspective Paper prepared for Symposium on the Mathematical Foundations of Computing Science, Gdansk, pp. 205\u2013214. Springer, Heidelberg (1976)"},{"key":"24_CR36","unstructured":"Feigenbaum, E.A., Feldman, J. (eds.): Computers & Thought. AAAI Press \/ MIT Press (1995)"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Franz\u00e9n, T.: G\u00f6del\u2019s Theorem. An Incomplete Guide to its Use and Abuse. A. K. Peters (2005)","DOI":"10.1201\/b10700"},{"key":"24_CR38","unstructured":"Gelerntner, H.: Realization of a geometry-theorem proving machine. In: Proceedings of the International Conference on Information Processing, UNESCO House, pp. 273\u2013282, 1959 Also appears in [94], pp. 99\u2013117 and in [36], pp. 134\u2013152 (1959)"},{"key":"24_CR39","doi-asserted-by":"crossref","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 Journal of research and development\u00a04, 28\u201335 (1960)","journal-title":"IBM Journal of research and development"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme, I. Monatshefte f\u00fcr Mathematik und Physik, vol. 38, 173\u2013198, English translation, On Formally Undecidable Propositions of Principia Mathematica and Related Systems, I In: [52], pp. 592\u2013618 or [30], pp. 4\u201338 (1931)","DOI":"10.1007\/BF01700692"},{"key":"24_CR41","first-page":"142","volume-title":"DATE 2002","author":"E. Goldberg","year":"2002","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a fast and robust Sat-solver. In: Kloos, C.D., Franca, J.D. (eds.) DATE 2002. Design, Automation and Test in Europe Conference and Exhibition, Paris, France, pp. 142\u2013149. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"24_CR42","volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"24_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M.J.C. Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"24_CR44","series-title":"Kluwer international series in engineering and computer science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3576-8","volume-title":"The SECD Microprocessor: A verification case study","author":"B.T. Graham","year":"1992","unstructured":"Graham, B.T.: The SECD Microprocessor: A verification case study. Kluwer international series in engineering and computer science, vol.\u00a0178. Kluwer Academic Publishers, Boston (1992)"},{"key":"24_CR45","doi-asserted-by":"crossref","unstructured":"Grothendieck, A.: \u00c9l\u00e9ments de G\u00e9om\u00e9trie Alg\u00e9braique IV: \u00c9tude locale de sch\u00e9mas et des morphismes de sch\u00e9mas, vol.\u00a020 of Publications Math\u00e9matiques. IHES (1964)","DOI":"10.1007\/BF02684747"},{"key":"24_CR46","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J.R. Guard","year":"1969","unstructured":"Guard, J.R., Oglesby, F.C., Bennett, J.H., Settle, L.G.: Semi-automated mathematics. Journal of the ACM\u00a016, 49\u201362 (1969)","journal-title":"Journal of the ACM"},{"key":"24_CR47","unstructured":"Hales, T.C.: The Kepler conjecture (1998), available at http:\/\/front.math.ucdavis.edu\/math.MG\/9811078"},{"key":"24_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0097791","volume-title":"Types for Proofs and Programs","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Proof style. In: Gim\u00e9nez, E., Paulin-Mohring, C. (eds.) TYPES 1996. LNCS, vol.\u00a01512, pp. 154\u2013172. Springer, Heidelberg (1998)"},{"key":"24_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11757283_8","volume-title":"Formal Methods for Hardware Verification","author":"J. Harrison","year":"2006","unstructured":"Harrison, J.: Floating-point verification using theorem proving. In: Bernardo, M., Cimatti, A. (eds.) SFM 2006. LNCS, vol.\u00a03965, pp. 211\u2013242. Springer, Heidelberg (2006)"},{"key":"24_CR50","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison, J., Th\u00e9ry, L.: A sceptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning\u00a021, 279\u2013294 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR51","first-page":"332","volume":"24","author":"P.J. Heawood","year":"1890","unstructured":"Heawood, P.J.: Map-colour theorem. Quarterly Journal of Pure and Applied Mathematics Reprinted in [8]\u00a024, 332\u2013338 (1890)","journal-title":"Quarterly Journal of Pure and Applied Mathematics Reprinted in [8]"},{"key":"24_CR52","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879\u20131931","year":"1967","unstructured":"Heijenoort, J.v. (ed.): From Frege to G\u00f6del: A Source Book in Mathematical Logic 1879\u20131931. Harvard University Press, Cambridge (1967)"},{"key":"24_CR53","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF01448445","volume":"88","author":"D. Hilbert","year":"1922","unstructured":"Hilbert, D.: Die logischen Grundlagen der Mathematik. Mathematische Annalen\u00a088, 151\u2013165 (1922)","journal-title":"Mathematische Annalen"},{"key":"24_CR54","first-page":"8","volume":"8","author":"J. Hintikka","year":"1955","unstructured":"Hintikka, J.: Form and content in quantification theory. Acta Philosophica Fennica \u2014 Two papers on Symbolic Logic\u00a08, 8\u201355 (1955)","journal-title":"Acta Philosophica Fennica \u2014 Two papers on Symbolic Logic"},{"key":"24_CR55","unstructured":"Hobbes, T.: Leviathan. Andrew Crooke (1651)"},{"key":"24_CR56","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G.: A complete proof of correctness of the Knuth-Bendix completion procedure. Journal of Computer and System Sciences\u00a023, 11\u201321 (1981)","journal-title":"Journal of Computer and System Sciences"},{"key":"24_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-57960-5","volume-title":"FM8501: A Verified Microprocessor","author":"W.A. Hunt","year":"1994","unstructured":"Hunt, W.A.: A Verified Micrprocessor. PhD thesis, University of Texas, 1985. In: Hunt Jr., W.A. (ed.) FM8501: A Verified Microprocessor. LNCS, vol.\u00a0795, Springer, Heidelberg (1994)"},{"key":"24_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"24_CR59","doi-asserted-by":"crossref","unstructured":"Joyce, J.J.: Formal verification and implementation of a microprocessor. In: Birtwistle and Subrahmanyam [9], pp. 129\u2013158","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"24_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/3-540-15976-2_17","volume-title":"Rewriting Techniques and Applications","author":"A. Kandri-Rody","year":"1985","unstructured":"Kandri-Rody, A., Kapur, D., Narendran, P.: An ideal-theoretic approach to word problems and unification problems over finitely presented commutative algebras. In: Jouannaud, J.-P. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a0202, pp. 345\u2013364. Springer, Heidelberg (1985)"},{"key":"24_CR61","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction in Geometry","author":"D. Kapur","year":"1998","unstructured":"Kapur, D.: Automated geometric reasoning: Dixon resultants, Gr\u00f6bner bases, and characteristic sets. In: Wang, D. (ed.) Automated Deduction in Geometry. LNCS, vol.\u00a01360, Springer, Heidelberg (1998)"},{"key":"24_CR62","doi-asserted-by":"publisher","first-page":"193","DOI":"10.2307\/2369235","volume":"2","author":"A.B. Kempe","year":"1879","unstructured":"Kempe, A.B.: On the geographical problem of the four colours. American Journal of Mathematics Reprinted in [8]\u00a02, 193\u2013200 (1879)","journal-title":"American Journal of Mathematics Reprinted in [8]"},{"key":"24_CR63","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, Pergamon Press, New York (1970)"},{"key":"24_CR64","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R.A. Kowalski","year":"1971","unstructured":"Kowalski, R.A., Kuehner, D.: Linear resolution with selection function. Artificial Intelligence\u00a02, 227\u2013260 (1971)","journal-title":"Artificial Intelligence"},{"key":"24_CR65","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1111\/j.1746-8361.1958.tb01469.x","volume":"12","author":"G. Kreisel","year":"1958","unstructured":"Kreisel, G.: Hilbert\u2019s programme. Dialectica Revised version in [6]\u00a012, 346\u2013372 (1958)","journal-title":"Dialectica Revised version in [6]"},{"key":"24_CR66","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/BF03023977","volume":"12","author":"C.W.H. Lam","year":"1990","unstructured":"Lam, C.W.H.: How reliable is a computer-based proof? The Mathematical Intelligencer\u00a012, 8\u201312 (1990)","journal-title":"The Mathematical Intelligencer"},{"key":"24_CR67","series-title":"Lecture Notes in Mathematics","volume-title":"Symposium on Automatic Demonstration","year":"1970","unstructured":"Laudet, M., Lacombe, D., Nolin, L., Sch\u00fctzenberger, M. (eds.): Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol.\u00a0125. Springer, Heidelberg (1970)"},{"key":"24_CR68","unstructured":"Lecat, M.: Erreurs de Math\u00e9maticiens des origines \u00e0 nos jours. Ancne Libraire Castaigne et Libraire \u00c9m Desbarax, Brussels (1935)"},{"key":"24_CR69","volume-title":"Littlewood\u2019s Miscellany Edited by Bela Bollobas","author":"J.E. Littlewood","year":"1986","unstructured":"Littlewood, J.E.: Littlewood\u2019s Miscellany Edited by Bela Bollobas. Cambridge University Press, Cambridge (1986)"},{"key":"24_CR70","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. Journal of the ACM\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"24_CR71","doi-asserted-by":"crossref","unstructured":"Loveland, D.W.: A linear format for resolution. In: Laudet, et al. [67], pp. 147\u2013162","DOI":"10.1007\/BFb0060630"},{"key":"24_CR72","doi-asserted-by":"crossref","unstructured":"Luckham, D.: Refinements in resolution theory. In: Laudet, et al. [67], pp. 163\u2013190","DOI":"10.1007\/BFb0060631"},{"key":"24_CR73","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4872-9","volume-title":"Mathematics: Form and Function","author":"S. Mac Lane","year":"1986","unstructured":"Mac Lane, S.: Mathematics: Form and Function. Springer, Heidelberg (1986)"},{"key":"24_CR74","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4529.001.0001","volume-title":"Mechanizing Proof: Computing, Risk and Trust","author":"D. MacKenzie","year":"2001","unstructured":"MacKenzie, D.: Mechanizing Proof: Computing, Risk and Trust. MIT Press, Cambridge (2001)"},{"key":"24_CR75","doi-asserted-by":"crossref","unstructured":"Marciszewski, W., Murawski, R.: Mechanization of Reasoning in a Historical Perspective, vol. 43 of Pozna\u0144 Studies in the Philosophy of the Sciences and the Humanities. Rodopi, Amsterdam (1995)","DOI":"10.1163\/9789004457423"},{"key":"24_CR76","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019, 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61398-6","volume-title":"Automated Deduction in Equational Logic and Cubic Curves","author":"W. McCune","year":"1996","unstructured":"McCune, W., Padmanabhan, R.: Automated Deduction in Equational Logic and Cubic Curves. LNCS, vol.\u00a01095. Springer, Heidelberg (1996)"},{"key":"24_CR78","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5 K 86 floating-point division program. IEEE Transactions on Computers\u00a047, 913\u2013926 (1998)","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR79","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/378239.379017","volume-title":"DAC 2001","author":"W. Moskewicz","year":"2001","unstructured":"Moskewicz, W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC 2001. Proceedings of the 38th Design Automation Conference, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"24_CR80","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR81","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/TIT.1956.1056797","volume":"2","author":"A. Newell","year":"1956","unstructured":"Newell, A., Simon, H.A.: The logic theory machine. IRE Transactions on Information Theory\u00a02, 61\u201379 (1956)","journal-title":"IRE Transactions on Information Theory"},{"key":"24_CR82","unstructured":"O\u2019Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, 1999-Q1, 1\u201314 (1999), available on the Web as http:\/\/developer.intel.com\/technology\/itj\/q11999\/articles\/art_5.htm"},{"key":"24_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-59293-8_189","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"V.R. Pratt","year":"1995","unstructured":"Pratt, V.R.: Anatomy of the Pentium bug. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 97\u2013107. Springer, Heidelberg (1995)"},{"key":"24_CR84","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. Journal of the ACM\u00a07, 102\u2013128 (1960)","journal-title":"Journal of the ACM"},{"key":"24_CR85","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich, Warszawa 1929, pp. 92\u2013101, 395. Warsaw, 1930. Annotated English version by [101] (1929)"},{"key":"24_CR86","series-title":"Lecture Notes in Computer Science","first-page":"195","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent programs in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol.\u00a0137, pp. 195\u2013220. Springer, Heidelberg (1982)"},{"key":"24_CR87","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. International Journal of Computer Mathematics\u00a01, 227\u2013234 (1965)","journal-title":"International Journal of Computer Mathematics"},{"key":"24_CR88","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"24_CR89","unstructured":"Robu, J.: Geometry Theorem Proving in the Frame of Theorema Project. PhD thesis, RISC-Linz (2002)"},{"key":"24_CR90","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Rusinoff","year":"1998","unstructured":"Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998), available on the Web at http:\/\/www.onr.com\/user\/russ\/david\/k7-div-sqrt.html","journal-title":"LMS Journal of Computation and Mathematics"},{"key":"24_CR91","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C.-J.H. Seger","year":"1995","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06, 147\u2013189 (1995)","journal-title":"Formal Methods in System Design"},{"key":"24_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-49519-3_7","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"1998","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 82\u201399. Springer, Heidelberg (1998)"},{"key":"24_CR93","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R.: Deciding combinations of theories. Journal of the ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"24_CR94","first-page":"1957","volume-title":"Automation of Reasoning \u2014 Classical Papers on Computational Logic","year":"1983","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning \u2014 Classical Papers on Computational Logic, vol.\u00a0I, pp. 1957\u20131966. Springer, Heidelberg (1983)"},{"key":"24_CR95","doi-asserted-by":"crossref","first-page":"547","DOI":"10.2140\/pjm.1970.34.547","volume":"34","author":"H. Simmons","year":"1970","unstructured":"Simmons, H.: The solution of a decision problem for several classes of rings. Pacific Journal of Mathematics\u00a034, 547\u2013557 (1970)","journal-title":"Pacific Journal of Mathematics"},{"key":"24_CR96","doi-asserted-by":"publisher","first-page":"349","DOI":"10.2307\/2274508","volume":"53","author":"S. Simpson","year":"1988","unstructured":"Simpson, S.: Partial realizations of Hilbert\u2019s program. Journal of Symbolic Logic\u00a053, 349\u2013363 (1988)","journal-title":"Journal of Symbolic Logic"},{"key":"24_CR97","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J.R. Slagle","year":"1967","unstructured":"Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. Journal of the ACM\u00a014, 687\u2013697 (1967)","journal-title":"Journal of the ACM"},{"key":"24_CR98","series-title":"Oxford Logic Guides","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195046724.001.0001","volume-title":"G\u00f6del\u2019s Incompleteness Theorems","author":"R.M. Smullyan","year":"1992","unstructured":"Smullyan, R.M.: G\u00f6del\u2019s Incompleteness Theorems. Oxford Logic Guides, vol.\u00a019. Oxford University Press, Oxford (1992)"},{"key":"24_CR99","first-page":"31","volume":"8","author":"M.K. Srivas","year":"1993","unstructured":"Srivas, M.K., Miller, S.P.: Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in System Design\u00a08, 31\u201336 (1993)","journal-title":"Formal Methods in System Design"},{"key":"24_CR100","first-page":"31","volume-title":"SAFECOMP 1990","author":"G. St\u00e5lmarck","year":"1990","unstructured":"St\u00e5lmarck, G., S\u00e4flund, M.: Modeling and verifying systems and software in propositional logic. In: Daniels, B.K. (ed.) SAFECOMP 1990. Safety of Computer Control Systems, Gatwick, UK, pp. 31\u201336. Pergamon Press, New York (1990)"},{"key":"24_CR101","unstructured":"Stansifer, R.: Presburger\u2019s article on integer arithmetic: Remarks and translation. Technical Report CORNELLCS:TR84-639, Cornell University Computer Science Department (1984)"},{"key":"24_CR102","unstructured":"Suttner, C.B., Sutcliffe, G.: The TPTP problem library. Technical Report AR-95-03, Institut f\u00fcr Infomatik, TU M\u00fcnchen, Germany, Also available as TR 95\/6 from Dept. Computer Science, James Cook University, Australia, and on the Web (1995)"},{"key":"24_CR103","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, 1951. Previous version published as a technical report by the RAND Corporation, 1948; prepared for publication by J. C. C. McKinsey. Reprinted in [21], pp. 24\u201384 (1951)","DOI":"10.1525\/9780520348097"},{"key":"24_CR104","first-page":"136","volume":"6","author":"A. Trybulec","year":"1978","unstructured":"Trybulec, A.: The Mizar-QC\/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing)\u00a06, 136\u2013140 (1978)","journal-title":"ALLC Bulletin (Association for Literary and Linguistic Computing)"},{"key":"24_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/3-540-15648-8_30","volume-title":"Logics of Programs","author":"A. Trybulec","year":"1985","unstructured":"Trybulec, A., Blair, H.A.: Computer aided reasoning. In: Parikh, R. (ed.) Logics of Programs. LNCS, vol.\u00a0193, pp. 406\u2013412. Springer, Heidelberg (1985)"},{"key":"24_CR106","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society (2)\u00a042, 230\u2013265 (1936)","journal-title":"Proceedings of the London Mathematical Society (2)"},{"key":"24_CR107","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H. Wang","year":"1960","unstructured":"Wang, H.: Toward mechanical mathematics. IBM Journal of research and development\u00a04, 2\u201322 (1960)","journal-title":"IBM Journal of research and development"},{"key":"24_CR108","first-page":"157","volume":"21","author":"W. Wen-ts\u00fcn","year":"1978","unstructured":"Wen-ts\u00fcn, W.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica\u00a021, 157\u2013179 (1978)","journal-title":"Scientia Sinica"},{"key":"24_CR109","volume-title":"Principia Mathematica (3 vols)","author":"A.N. Whitehead","year":"1910","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica (3 vols). Cambridge University Press, Cambridge (1910)"},{"key":"24_CR110","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"},{"key":"24_CR111","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L. Wos","year":"1999","unstructured":"Wos, L., Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, Singapore (1999)"}],"container-title":["Lecture Notes in Computer Science","Algebraic Biology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73433-8_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T19:20:17Z","timestamp":1684005617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73433-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540734321","9783540734338"],"references-count":111,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73433-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}