{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:53:10Z","timestamp":1760597590377},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642413599"},{"type":"electronic","value":"9783642413605"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41360-5_9","type":"book-chapter","created":{"date-parts":[[2013,9,7]],"date-time":"2013-09-07T03:03:50Z","timestamp":1378523030000},"page":"102-116","source":"Crossref","is-referenced-by-count":8,"title":["Exploring Automated Reasoning in First-Order Logic: Tools, Techniques and Application Areas"],"prefix":"10.1007","author":[{"given":"Vladimir","family":"Pavlov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Schukin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tanzilia","family":"Cherkasova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Avigad, J., et al.: A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (TOCL)\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297660"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-63385-5_28","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1997","unstructured":"Bachmair, L.: Paramodulation, superposition, and simplification. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol.\u00a01289, pp. 1\u20133. Springer, Heidelberg (1997)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 19\u201399 (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61630-6_1","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol.\u00a01126, pp. 1\u201317. Springer, Heidelberg (1996)"},{"issue":"1","key":"9_CR5","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\u00a09(1), 1\u201335 (1977)","journal-title":"Artificial Intelligence"},{"key":"9_CR6","unstructured":"Bridge, J.P.: Machine learning and automated theorem proving. Technical Report, Cambridge (2010), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-792.pdf"},{"key":"9_CR7","unstructured":"Chen, C., Li, R.: Matematicheskaya logika I avtomaticheskoe dokazatel\u2019stvo teorem (Russian) (Mathematical Logic and Automatic Theorem Proving). In: Translated from English by Davydov, G. V., Mints, G. E., Sochilina, A. V. Edited by Maslov, S.Y. With appendixes by Maslov, S.Y., Mints, G.E., Orevkov, V. P. Nauka, Moscow (1983)"},{"key":"9_CR8","unstructured":"Chlipala, A., Necula, G.C.: Cooperative Integration of an Interactive Proof Assistant and an Automated Prover. In: Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006 (2006)"},{"issue":"7","key":"9_CR9","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 179\u2013272 (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"issue":"2","key":"9_CR11","first-page":"87","volume":"44","author":"D. Dumitrescu","year":"1999","unstructured":"Dumitrescu, D., Oltean, M.: An Evolutionary Algorithm for Theorem Proving in Propositional Logic. Studia Universitatis Babes-Bolyai, Informatica\u00a044(2), 87\u201398 (1999)","journal-title":"Studia Universitatis Babes-Bolyai, Informatica"},{"key":"9_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-69912-5_14","volume-title":"KI 2006: Advances in Artificial Intelligence","author":"U. Furbach","year":"2007","unstructured":"Furbach, U., Obermaier, C.: Applications of Automated Reasoning. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol.\u00a04314, pp. 174\u2013187. Springer, Heidelberg (2007)"},{"key":"9_CR13","unstructured":"Gebser, M., et al.: Conflict-driven answer set solving. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 386\u2013392 (2007)"},{"key":"9_CR14","unstructured":"Gonthier, G.: A computer-checked proof of the Four Colour Theorem. Microsoft Research Cambridge (2005), \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/people\/gonthier\/4colproof.pdf"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Engineering mathematics: the odd order theorem proof. In: POPL 2013, pp. 1\u20132 (2013)","DOI":"10.1145\/2480359.2429071"},{"key":"9_CR16","unstructured":"Hagen, R.A., Goodwin, S., Sattar, A.: Code improvements for model elimination based reasoning systems. In: Proceedings of the 27th Australasian Conference on Computer Science, ACSC 2004, vol.\u00a026, pp. 233\u2013240 (2004)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Tableaux and Related Methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, pp. 101\u2013177 (2001)","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-73433-8_24","volume-title":"Algebraic Biology","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: A short survey of automated reasoning. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) AB 2007. LNCS, vol.\u00a04545, pp. 334\u2013349. Springer, Heidelberg (2007)"},{"key":"9_CR19","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":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-44659-1_15","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 234\u2013251. Springer, Heidelberg (2000)"},{"key":"9_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J. Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, New York (2009)"},{"issue":"4","key":"9_CR22","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1023\/A:1006350622830","volume":"24","author":"H.H. Hoops","year":"2000","unstructured":"Hoops, H.H., St\u00fctzle, T.: Local Search Algorithms for SAT: An Empirical Evaluation. Journal of Automated Reasoning\u00a024(4), 421\u2013481 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Patel-Schneider, P.F.: Knowledge Representation and Reasoning on the Semantic Web: OWL. In: Domingue, J., Fensel, D., Hendler, J.A. (eds.) Handbook of Semantic Web Technologies, pp. 365\u2013398. Springer (2011)","DOI":"10.1007\/978-3-540-92913-0_9"},{"key":"9_CR24","unstructured":"Katsiri, E., Mycroft, A.: Model checking for sentient computing: An axiomatic approach. In: Proceedings of the 1st Workshop on Semantics for Mobile Environments, SME 2005 (2005), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/research\/dtg\/www\/files\/publications\/public\/ek236\/satisfiability6.pdf"},{"key":"9_CR25","unstructured":"Kaufmann, M., Moore, J.S.: Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification. In: Revista de la Real Academia de Ciencias Exactas, F\u00edsicas y Naturales. Serie A: Matem\u00e1ticas (RACSAM)\u00a098(1\/2), 181\u2013195 (2004) ISSN 1578-7303"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/978-3-642-34481-7_82","volume-title":"Neural Information Processing","author":"M. Khalifa","year":"2012","unstructured":"Khalifa, M., Raafat, H., Almulla, M.: Machine Learning Approach to Enhance the Design of Automated Theorem Provers. In: Huang, T., Zeng, Z., Li, C., Leung, C.S. (eds.) ICONIP 2012, Part II. LNCS, vol.\u00a07664, pp. 673\u2013682. Springer, Heidelberg (2012)"},{"key":"9_CR27","unstructured":"Kornilowicz, A.: Formalization of the Jordan Curve Theorem in Mizar. In: International Congress of Mathematicians, Volume of Abstracts, p. 611 (2006)"},{"key":"9_CR28","unstructured":"Kowalski, R.: Predicate Logic as a Programming Language. In: Proceedings of the IFIP Congress, pp. 569\u2013574 (1974)"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015\u20132112 (2001)","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"issue":"1","key":"9_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00245018","volume":"5","author":"V. Lifschitz","year":"1989","unstructured":"Lifschitz, V.: What is the inverse method? Journal of Automated Reasoning\u00a05(1), 1\u201323 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"9_CR31","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(2), 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"issue":"pt.I","key":"9_CR32","first-page":"26","volume":"98","author":"S.Y. Maslov","year":"1968","unstructured":"Maslov, S.Y.: The inverse method for establishing deducibility for logical calculi. Logical and logical-mathematical calculus (Russian). Trudy Mat. Inst. Steklov.\u00a098(pt.I), 26\u201387 (1968)","journal-title":"Trudy Mat. Inst. Steklov."},{"issue":"3","key":"9_CR33","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(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR34","unstructured":"Meng, J.: Integration of interactive and automatic provers. In: Second CologNet Workshop on Implementation Technology Computational Logic Systems (2003)"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-642-15025-8_26","volume-title":"Fields of Logic and Computation","author":"G. Mints","year":"2010","unstructured":"Mints, G.: Decidability of the Class E by Maslov\u201ds Inverse Method. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Gurevich Festschrift. LNCS, vol.\u00a06300, pp. 529\u2013537. Springer, Heidelberg (2010)"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-48885-5_19","volume-title":"Genetic Programming","author":"P. Nordin","year":"1999","unstructured":"Nordin, P., Eriksson, A., Nordahl, M.G.: Genetic Reasoning: Evolutionary Induction of Mathematical Proofs. In: Langdon, W.B., Fogarty, T.C., Nordin, P., Poli, R. (eds.) EuroGP 1999. LNCS, vol.\u00a01598, pp. 221\u2013231. Springer, Heidelberg (1999)"},{"issue":"2-3","key":"9_CR37","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10817-007-9089-7","volume":"40","author":"A. Paskevich","year":"2008","unstructured":"Paskevich, A.: Connection Tableaux with Lazy Paramodulation. Journal of Automated Reasoning\u00a040(2-3), 179\u2013194 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 97\u2013107. Springer, Heidelberg (1995)"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Reed, J.N., Sinclair, J.E., Guigand, F.: Deductive Reasoning versus Model Checking: Two Formal Approaches for System Development. In: Proceedings of the 1st International Conference on Integrated Formal Methods (IFM), pp. 375\u2013394 (1999)","DOI":"10.1007\/978-1-4471-0851-1_20"},{"key":"9_CR40","first-page":"23","volume":"5","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A Machine-Oriented Logic Based on the Resolution Principle. Communications of the ACM\u00a05, 23\u201341 (1965)","journal-title":"Communications of the ACM"},{"issue":"2\/3","key":"9_CR41","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"9_CR42","unstructured":"Smullyan, R.M.: First-Order Logic. Courier Dover Publications (1995)"},{"key":"9_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-69149-5_55","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Stump","year":"2008","unstructured":"Stump, A.: Programming with Proofs: Language-Based Approaches to Totally Correct Software. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 502\u2013509. Springer, Heidelberg (2008)"},{"issue":"1","key":"9_CR44","first-page":"121","volume":"23","author":"J. Sutcliffe","year":"2002","unstructured":"Sutcliffe, J.: Automated theorem proving: theory and practice. AI Magazine\u00a023(1), 121\u2013122 (2002)","journal-title":"AI Magazine"},{"issue":"2","key":"9_CR45","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"J. Sutcliffe","year":"1988","unstructured":"Sutcliffe, J., Suttner, C.: The TPTP Problem Library. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1988)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"9_CR46","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1017\/S144618110000300X","volume":"48","author":"G. Szekeres","year":"2006","unstructured":"Szekeres, G., Peters, L.: Computer solution to the 17-point Erd\u0151s-Szekeres problem. ANZIAM Journal\u00a048(2), 151\u2013164 (2006)","journal-title":"ANZIAM Journal"},{"key":"9_CR47","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-73595-3_11","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Tiwari","year":"2007","unstructured":"Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 147\u2013166. Springer, Heidelberg (2007)"},{"key":"9_CR48","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-540-71070-7_37","volume-title":"Automated Reasoning","author":"J. Urban","year":"2008","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 441\u2013456. Springer, Heidelberg (2008)"}],"container-title":["Communications in Computer and Information Science","Knowledge Engineering and the Semantic Web"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41360-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T22:48:03Z","timestamp":1558046883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41360-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642413599","9783642413605"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41360-5_9","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2013]]}}}