{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T05:52:23Z","timestamp":1768456343052,"version":"3.49.0"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319486277","type":"print"},{"value":"9783319486284","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-48628-4_9","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T12:45:31Z","timestamp":1488372331000},"page":"211-241","source":"Crossref","is-referenced-by-count":10,"title":["Advances in Connection-Based Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"Jens","family":"Otten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Bibel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"9_CR1","unstructured":"http:\/\/www.scientificamerican.com\/article\/pogue-5-most-embarrassing-software-bugs-in-history\/ . Accessed 15 June 2016"},{"key":"9_CR2","unstructured":"https:\/\/en.wikipedia.org\/wiki\/2015_Seville_Airbus_A400M_Atlas_crash . Accessed 15 June 2016"},{"key":"9_CR3","unstructured":"https:\/\/en.wikipedia.org\/wiki\/List_of_failed_and_overbudget_custom_software_projects . Accessed 15 June 2016"},{"key":"9_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-006-9055-9","volume":"38","author":"R Antonsen","year":"2007","unstructured":"Antonsen, R., Waaler, A.: Liberalized variable splitting. J. Autom. Reason. 38, 3\u201330 (2007)","journal-title":"J. Autom. Reason."},{"key":"9_CR5","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-94-011-3488-0_2","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"O Astrachan","year":"1991","unstructured":"Astrachan, O., Loveland, D.: METEORs: high performance theorem provers using model elimination. In: Bledsoe, W., Boyer, S. (eds.) Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 31\u201360. Kluwer, Amsterdam (1991)"},{"key":"9_CR6","unstructured":"Andrews, P.B.: General matings. In: Joyner, W.H. (ed.) Fourth Workshop on Automated Deduction, pp. 19\u201325 (1979)"},{"key":"9_CR7","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"PB Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. J. ACM 28, 193\u2013214 (1981)","journal-title":"J. ACM"},{"key":"9_CR8","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0049-237X(08)71097-8","volume-title":"Handbook of Mathematical Logic","author":"J Barwise","year":"1977","unstructured":"Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 5\u201346. North-Holland, Amsterdam (1977)"},{"key":"9_CR9","volume-title":"Handbook of Modal Logic","author":"P Blackburn","year":"2006","unstructured":"Blackburn, P., van Bentham, J., Wolter, F.: Handbook of Modal Logic. Elsevier, Amsterdam (2006)"},{"key":"9_CR10","series-title":"Applied Logic Series 19","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-94-015-9383-0_2","volume-title":"Intellectics and Computational Logic","author":"P Baumgartner","year":"2000","unstructured":"Baumgartner, P., Eisinger, N., Furbach, U.: A confluent connection calculus. In: H\u00f6lldobler, S. (ed.) Intellectics and Computational Logic. Applied Logic Series 19, pp. 3\u201326. Kluwer, Dordrecht (2000)"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF02239498","volume":"12","author":"W Bibel","year":"1974","unstructured":"Bibel, W.: An approach to a systematic theorem proving procedure in first-order logic. Computing 12, 43\u201355 (1974)","journal-title":"Computing"},{"key":"9_CR12","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0004-3702(80)90050-8","volume":"14","author":"W Bibel","year":"1980","unstructured":"Bibel, W.: Syntax-directed, semantics-supported program synthesis. Artificial Intelligence 14, 243\u2013261 (1980)","journal-title":"Artificial Intelligence"},{"key":"9_CR13","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections. J. ACM 28, 633\u2013645 (1981)","journal-title":"J. ACM"},{"key":"9_CR14","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices. Commun. ACM 26, 844\u2013852 (1983)","journal-title":"Commun. ACM"},{"key":"9_CR15","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, Braunschweig (1987)","edition":"2"},{"key":"9_CR16","series-title":"Action, and Interaction in AI Theories and Systems - Essays dedicated to Luigia Carlucci Aiello, LNAI 4155","first-page":"25","volume-title":"Reasoning","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 - Essays dedicated to Luigia Carlucci Aiello, LNAI 4155, pp. 25\u201343. Springer, Berlin (2006)"},{"key":"9_CR17","series-title":"LNAI 4667","first-page":"2","volume-title":"KI 2007","author":"W Bibel","year":"2007","unstructured":"Bibel, W.: Early history and perspectives of automated deduction. In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007. LNAI 4667, pp. 2\u201318. Springer, Berlin (2007)"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Bibel, W., Br\u00fcning, S., Egly, U., Rath, T.: In: Bundy, A. (ed.) CADE-12. LNAI 814, pp. 783\u2013787. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58156-1_60"},{"key":"9_CR19","unstructured":"Bibel, W., Otten, J.: From sch\u00fctte\u2019s formal system to modern automated deduction. In: Kahle, R.,\u00a0Rathjen, M. (eds.), The Legacy of Kurt Sch\u00fctte. Springer, London, to appear"},{"key":"9_CR20","series-title":"LNAI 6463","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-642-17172-7_3","volume-title":"Verification, Induction, Termination Analysis","author":"C Brandt","year":"2010","unstructured":"Brandt, C., Otten, J., Kreitz, C., Bibel, W.: Specifying and verifying organizational security properties in first-order logic. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNAI 6463, pp. 38\u201353. Springer, Heidelberg (2010)"},{"key":"9_CR21","first-page":"163","volume-title":"20th European Conference on Artificial Intelligence (ECAI 2012)","author":"C Benzm\u00fcller","year":"2012","unstructured":"Benzm\u00fcller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: De Raedt, L., et al. (eds.) 20th European Conference on Artificial Intelligence (ECAI 2012), pp. 163\u2013168. IOS Press, Amsterdam (2012)"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing, pp. 151\u2013158. ACM, New York (1971)","DOI":"10.1145\/800157.805047"},{"key":"9_CR23","first-page":"224","volume-title":"The Blackwell Guide to Philosophical Logic","author":"D Dalen van","year":"2001","unstructured":"van Dalen, D.: Intuitionistic logic. In: Goble, L. (ed.) The Blackwell Guide to Philosophical Logic, pp. 224\u2013257. Blackwell, Oxford (2001)"},{"key":"9_CR24","volume-title":"Logic Programming, Systematic Program Development","author":"Y Deville","year":"1990","unstructured":"Deville, Y.: Logic Programming, Systematic Program Development. Addison-Wesley, Wokingham (1990)"},{"key":"9_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-84222-0","volume-title":"Relative Complexities of First Order Calculi","author":"E Eder","year":"1992","unstructured":"Eder, E.: Relative Complexities of First Order Calculi. Vieweg, Braunschweig (1992)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Fisher, K.: HACMS: high assurance cyber military systems. In: Proceedings of the 2012 ACM Conference on High Integrity Language Technoloby, pp. 51\u201352. ACM, New York (2012)","DOI":"10.1145\/2402676.2402695"},{"key":"9_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logic","author":"M Fitting","year":"1983","unstructured":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logic. D. Reidel, Dordrecht (1983)"},{"key":"9_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"issue":"176\u2013210","key":"9_CR29","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Math. Z. 39(176\u2013210), 405\u2013431 (1935)","journal-title":"Math. Z."},{"key":"9_CR30","volume-title":"Provably Correct Systems","author":"S Goel","year":"2016","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M.: Engineering a formal, executable x86 ISA simulator for software verification. In: Bowen, J.P., Hinchey, M., Olderog, E.-R. (eds.) Provably Correct Systems. Springer, London (2016)"},{"key":"9_CR31","first-page":"100","volume-title":"Handbook of Automated Reasoning","author":"R H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100\u2013178. Elsevier, Amsterdam (2001)"},{"key":"9_CR32","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1016\/j.tcs.2004.09.001","volume":"328","author":"R H\u00e4hnle","year":"2004","unstructured":"H\u00e4hnle, R., Murray, N.V., Rosenthal, E.: Linearity and regularity with negation normal form. Theor. Comput. Sci. 328, 325\u2013354 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR33","unstructured":"Hansen, C.: A Variable Splitting Theorem Prover. University of Oslo (2012)"},{"key":"9_CR34","unstructured":"Herbrand, J.J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 Mathem. Phys. (1930)"},{"key":"9_CR35","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/358549.358561","volume":"24","author":"CAR Hoare","year":"1981","unstructured":"Hoare, C.A.R.: The emperor\u2019s old clothes. Commun. ACM 24, 75\u201383 (1981)","journal-title":"Commun. ACM"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Adronick, J., Cock, D.,\u00a0Derrin, P.,\u00a0Elkaduwe, D.,\u00a0Engelhardt, K.,\u00a0Kolanski, R.,\u00a0Norrish, M.,\u00a0Sewell, T.,\u00a0Tuch, H.,\u00a0Winwood, S.: SeL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM SIGOPS, pp. 207\u2013220. ACM, New York (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"9_CR37","first-page":"25","volume":"9","author":"S-J Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating duplicates with the hyper-linking strategy. J. Autom. Reason. 9, 25\u201342 (1992)","journal-title":"J. Autom. Reason."},{"key":"9_CR38","doi-asserted-by":"crossref","first-page":"2015","DOI":"10.1016\/B978-044450813-3\/50030-8","volume-title":"Handbook of Automated Reasoning","author":"R Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model elimination and connection Tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015\u20132114. Elsevier, Amsterdam (2001)"},{"key":"9_CR39","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8, 183\u2013212 (1992)","journal-title":"J. Autom. Reason."},{"key":"9_CR40","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D Loveland","year":"1968","unstructured":"Loveland, D.: Mechanical theorem proving by model elimination. J. ACM 15, 236\u2013251 (1968)","journal-title":"J. ACM"},{"key":"9_CR41","unstructured":"McCune, W.: Release of Prover9. Mile High Conference on Quasigroups, Loops and Nonassociative Systems. Technical report, Denver (2005)"},{"key":"9_CR42","series-title":"LNCS 5663","first-page":"230","volume-title":"CADE-22","author":"S McLaughlin","year":"2009","unstructured":"McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Schmidt, R.A. (ed.) CADE-22. LNCS 5663, pp. 230\u2013244. Springer, Heidelberg (2009)"},{"key":"9_CR43","volume-title":"Provably Correct Systems","author":"JS Moore","year":"2016","unstructured":"Moore, J.S.: Computing verified machine address bounds during symbolic simulation of code. In: Bowen, J.P., Hinchey, M., Olderog, E.-R. (eds.) Provably Correct Systems. Springer, London (2016)"},{"key":"9_CR44","series-title":"LNAI 3702","first-page":"245","volume-title":"TABLEAUX 2005","author":"J Otten","year":"2005","unstructured":"Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNAI 3702, pp. 245\u2013261. Springer, Heidelberg (2005)"},{"key":"9_CR45","series-title":"LNCS 5195","first-page":"283","volume-title":"IJCAR 2008","author":"J Otten","year":"2008","unstructured":"Otten, J.: $${{ leanCoP}}$$ 2.0 and $${{ ileanCoP}}$$ 1.2: high performance lean theorem proving in classical and intuitionistic logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS 5195, pp. 283\u2013291. Springer, Heidelberg (2008)"},{"key":"9_CR46","doi-asserted-by":"crossref","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23, 159\u2013182 (2010)","journal-title":"AI Commun."},{"key":"9_CR47","series-title":"LNAI 6793","first-page":"226","volume-title":"TABLEAUX 2011","author":"J Otten","year":"2011","unstructured":"Otten, J.: A Non-clausal Connection Calculus. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) TABLEAUX 2011. LNAI 6793, pp. 226\u2013241. Springer, Heidelberg (2011)"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Otten, J.: Implementing connection calculi for first-order modal logics. In: Ternovska, E.,\u00a0Korovin, K.,\u00a0Schulz, S. (eds.), 9th International Workshop on the Implementation of Logics (IWIL 2012), EPiC, EasyChair, vol.\u00a022, pp. 18\u201332 (2012)","DOI":"10.29007\/82m9"},{"key":"9_CR49","series-title":"LNAI 8562","first-page":"269","volume-title":"IJCAR 2014","author":"J Otten","year":"2014","unstructured":"Otten, J.: $${{ MleanCoP}}$$ : a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNAI 8562, pp. 269\u2013276. Springer, Heidelberg (2014)"},{"key":"9_CR50","volume-title":"IJCAR 2016, LNAI 9706","author":"J Otten","year":"2016","unstructured":"Otten, J.: $${{ nanoCoP}}$$ : a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNAI 9706. Springer, Heidelberg (2016)"},{"key":"9_CR51","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: $${{ leanCoP}}$$ : lean connection-based theorem proving. J. Symb. Comput. 36, 139\u2013161 (2003)","journal-title":"J. Symb. Comput."},{"key":"9_CR52","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"9_CR53","series-title":"Lecture Notes in Mathem","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BFb0060634","volume-title":"Symposium on Automatic Demonstration","author":"D Prawitz","year":"1970","unstructured":"Prawitz, D.: A proof procedure with matrix reduction. In: Laudet, M., et al. (eds.) Symposium on Automatic Demonstration. Lecture Notes in Mathem, pp. 207\u2013214. Springer, Berlin (1970)"},{"key":"9_CR54","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-1221-3","volume-title":"A Concise Introduction to Mathematical Logic","author":"W Rautenberg","year":"2010","unstructured":"Rautenberg, W.: A Concise Introduction to Mathematical Logic. Springer, Heidelberg (2010)"},{"key":"9_CR55","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-006-9060-z","volume":"38","author":"T Raths","year":"2007","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP problem library for intuitionistic logic. J. Autom. Reason. 38, 261\u2013271 (2007)","journal-title":"J. Autom. Reason."},{"key":"9_CR56","series-title":"LNAI 7364","first-page":"454","volume-title":"IJCAR 2012","author":"T Raths","year":"2012","unstructured":"Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., et al. (eds.) IJCAR 2012. LNAI 7364, pp. 454\u2013461. Springer, Heidelberg (2012)"},{"key":"9_CR57","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"9_CR58","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-5998-0","volume-title":"Scalable Techniques for Formal Verification","author":"S Ray","year":"2010","unstructured":"Ray, S.: Scalable Techniques for Formal Verification. Springer, Heidelberg (2010)"},{"key":"9_CR59","series-title":"Applied Logic Series 19","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-94-015-9383-0_17","volume-title":"Intellectics and Computational Logic","author":"JA Robinson","year":"2000","unstructured":"Robinson, J.A.: Proof $$=$$ guarantee $$+$$ explanation. In: H\u00f6lldobler, S. (ed.) Intellectics and Computational Logic. Applied Logic Series 19, pp. 277\u2013294. Kluwer, Dordrecht (2000)"},{"key":"9_CR60","volume-title":"Handbook of Automated Reasoning","author":"JA Robinson","year":"2001","unstructured":"Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"key":"9_CR61","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"9_CR62","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"RM Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)"},{"key":"9_CR63","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","volume":"9","author":"R Statman","year":"1979","unstructured":"Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theoret. Comput. Sci. 9, 67\u201372 (1979)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR64","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M Stickel","year":"1988","unstructured":"Stickel, M.: A Prolog technology theorem prover: implementation by an extended Prolog compiler. J. Autom. Reason. 4, 353\u2013380 (1988)","journal-title":"J. Autom. Reason."},{"key":"9_CR65","first-page":"71","volume":"21","author":"G Sutcliffe","year":"2008","unstructured":"Sutcliffe, G.: The CADE-21 automated theorem proving system competition. AI Commun. 21, 71\u201381 (2008)","journal-title":"AI Commun."},{"key":"9_CR66","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43, 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9_CR67","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The CADE-22 automated theorem proving system competition - CASC-22. AI Commun. 23, 47\u201359 (2010)","journal-title":"AI Commun."},{"key":"9_CR68","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition - CASC-J5. AI Commun. 24, 75\u201389 (2011)","journal-title":"AI Commun."},{"key":"9_CR69","doi-asserted-by":"crossref","first-page":"1487","DOI":"10.1016\/B978-044450813-3\/50024-2","volume-title":"Handbook of Automated Reasoning","author":"A Waaler","year":"2001","unstructured":"Waaler, A.: Connections in nonclassical logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1487\u20131578. Elsevier, Amsterdam (2001)"},{"key":"9_CR70","volume-title":"Automated Deduction in Nonclassical Logics","author":"LA Wallen","year":"1990","unstructured":"Wallen, L.A.: Automated Deduction in Nonclassical Logics. MIT Press, Cambridge (1990)"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T22:19:26Z","timestamp":1750025966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_9","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"value":"1860-0131","type":"print"},{"value":"2197-6597","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}