{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T04:04:30Z","timestamp":1750565070720,"version":"3.41.0"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"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-63046-5_19","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"310-325","source":"Crossref","is-referenced-by-count":8,"title":["Detecting Inconsistencies in Large First-Order Knowledge Bases"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Schulz","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Pease","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR2","unstructured":"Alemi, A.A., Chollet, F., E\u00e9n, N., Irving, G., Szegedy, C., Urban, J.: DeepMath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., Luxburg, U.V., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 5\u201310, 2016, Barcelona, Spain, pp. 2235\u20132243 (2016). http:\/\/papers.nips.cc\/paper\/6280-deepmath-deep-sequence-models-for-premise-selection"},{"key":"19_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-30370-3","volume-title":"Principles of Health Interoperability: SNOMED CT, HL7 and FHIR (Health Information Technology Standards)","author":"T Benson","year":"2016","unstructured":"Benson, T.: Principles of Health Interoperability: SNOMED CT, HL7 and FHIR (Health Information Technology Standards). Springer, London (2016)"},{"key":"19_CR4","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Automating g\u00f6del\u2019s ontological proof of god\u2019s existence with higher-order automated theorem provers. In: Schaub, T. (ed.) Proceedings of the 21st European Conference on Artificial Intelligence, pp. 93\u201398 (2014)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162\u2013170. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_14"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Benzmller, C., Pease, A.: Higher-order aspects and context in SUMO. In: Jos Lehmann, I.J.V., Bundy, A. (eds.) Special issue on Reasoning with context in the Semantic Web, vol. 12\u201313. Science, Services and Agents on the World Wide Web (2012)","DOI":"10.1016\/j.websem.2011.11.008"},{"issue":"1","key":"19_CR7","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016). http:\/\/dx.doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reasoning"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14052-5_11"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-22438-6_13","volume-title":"Automated Deduction \u2013 CADE-23","author":"CE Brown","year":"2011","unstructured":"Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT problems. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 147\u2013161. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_13"},{"key":"19_CR10","unstructured":"Chaudhri, V., Inclezan, D.: Representing states in a biology textbook. In: Leora Morgenstern, L., Patkos, T., Sloan, R. (eds.) Proceedings of 12th International Symposium on Logical Formalizations of Commonsense Reasoning. AAAI Press (2015)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Farzan, A. (eds.): Proceedings of the 28th International Conference on Computer Aided Verification. LNCS, vol. 9779\u20139780. Springer, Heidelberg (2016)","DOI":"10.1007\/978-3-319-41528-4"},{"issue":"2","key":"19_CR12","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Korni\u0142owicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formalized Reasoning 3(2), 153\u2013245 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"19_CR13","unstructured":"Groth, P., Simperi, E., Gray, A., Sabou, M., Kr\u00f6tzsch, M., Lecue, F., Fl\u00f6ck, F., Gil, Y. (eds.): Proceedings of the 15th International Semantic Web Conference. LNCS, vol. 9981\u20139982. Springer, Heidelberg (2016)"},{"key":"19_CR14","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., et al.: A formal proof of the Kepler conjecture. arXiv preprint (2015). arXiv:1501.02155"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_23"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: Stronger automation for Flyspeck by feature weighting and strategy evolution. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. EPiC Series, vol. 14, pp. 87\u201395. EasyChair (2013)","DOI":"10.29007\/5gzr"},{"issue":"2","key":"19_CR17","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"issue":"3","key":"19_CR18","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3), 245\u2013256 (2015). http:\/\/dx.doi.org\/10.1007\/s10817-015-9330-8","journal-title":"J. Autom. Reasoning"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-36675-8_8","volume-title":"Automated Reasoning and Mathematics","author":"M Kinyon","year":"2013","unstructured":"Kinyon, M., Veroff, R., Vojt\u011bchovsk\u00fd, P.: Loops with abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 151\u2013164. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36675-8_8"},{"key":"19_CR20","unstructured":"Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs (2010). https:\/\/www.isa-afp.org\/"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_1"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31365-3_30","volume-title":"Automated Reasoning","author":"D K\u00fchlwein","year":"2012","unstructured":"K\u00fchlwein, D., Laarhoven, T., Tsivtsivadze, E., Urban, J., Heskes, T.: Overview and evaluation of premise selection techniques for large theory mathematics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 378\u2013392. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_30"},{"issue":"11","key":"19_CR23","first-page":"35","volume":"38","author":"D Lenat","year":"1995","unstructured":"Lenat, D.: CYC: a large-scale investment in knowledge infrastructure. Commun. ACM 38(11), 35\u201338 (1995)","journal-title":"Commun. ACM"},{"issue":"3","key":"19_CR24","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W McCune","year":"1997","unstructured":"McCune, W.: Solution of the robbins problem. J. Autom. Reasoning 19(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"19_CR25","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logics 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Logics"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Toward a standard upper ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems (FOIS-2001) (2001)","DOI":"10.1145\/505168.505170"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Paulsson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliff, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, vol. 2 (2012)","DOI":"10.29007\/36dt"},{"key":"19_CR28","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 61\u201370. No. 257 in CEUR Workshop Proceedings (2007)"},{"key":"19_CR29","volume-title":"Ontology: A Practical Guide","author":"A Pease","year":"2011","unstructured":"Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)"},{"key":"19_CR30","doi-asserted-by":"crossref","first-page":"9","DOI":"10.3233\/AIC-120549","volume":"26","author":"A Pease","year":"2013","unstructured":"Pease, A., Benzm\u00fcller, C.: Sigma: an integrated development environment for logical theories. AI Commun. 26, 9\u201397 (2013)","journal-title":"AI Commun."},{"key":"19_CR31","unstructured":"Pease, A., Niles, I., Li, J.: The suggested upper merged ontology: a large ontology for the semantic web and its applications. In: Working Notes of the AAAI-2002 Workshop on Ontologies and the Semantic Web (2002)"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Priest, G.: Paraconsistent logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 6, pp. 287\u2013393. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-017-0460-1_4"},{"key":"19_CR33","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: expressiveness and efficiency in a common sense knowledge base. In: Shvaiko, P. (ed.) Proceedings of the AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications (C&O-2005) (2005)"},{"key":"19_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-319-40229-1_10","volume-title":"Automated Reasoning","author":"A Reynolds","year":"2016","unstructured":"Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in SMT. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 133\u2013151. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_10"},{"issue":"2\/3","key":"19_CR35","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - A brainiac theorem prover. J. AI Commun. 15(2\/3), 111\u2013126 (2002)","journal-title":"J. AI Commun."},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_49"},{"key":"19_CR37","volume-title":"Formal Verification: An Essential Toolkit for Modern VLSI Design","author":"E Seligman","year":"2015","unstructured":"Seligman, E., Schubert, T., Achutha Kiran Kumar, M.: Formal Verification: An Essential Toolkit for Modern VLSI Design. Morgan Kaufmann, San Francisco (2015)"},{"issue":"1","key":"19_CR38","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/AIC-2012-0512","volume":"25","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G.: The CADE-23 automated theorem proving system competition - CASC-23. AI Commun. 25(1), 49\u201363 (2012)","journal-title":"AI Commun."},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reasoning. (2017, to appear)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"19_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: SRASS - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 295\u2013310. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73595-3_20"},{"key":"19_CR41","unstructured":"Sutcliffe, G., Urban, J., Schulz, S. (eds.): Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, CEUR Workshop Proceedings, vol. 257 (2007)"},{"issue":"1","key":"19_CR42","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Urban, J.: BliStr: The blind strategymaker. In: Gottlob, G., Sutcliffe, G., Voronkov, A. (eds.) Proceedings of the Global Conference on Artificial Intelligence, Tibilisi, Georgia. EPiC, vol. 36, pp. 312\u2013319. EasyChair (2015)","DOI":"10.29007\/8n7m"},{"issue":"2","key":"19_CR44","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s10817-012-9269-y","volume":"50","author":"J Urban","year":"2013","unstructured":"Urban, J., Rudnicki, P., Sutcliffe, G.: ATP and presentation service for Mizar formalizations. J. Autom. Reasoning 50(2), 229\u2013241 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR45","series-title":"Lecture Notes in Computer Science (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. 5195, pp. 441\u2013456. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_37"},{"issue":"2","key":"19_CR46","first-page":"227","volume":"36","author":"E Zalta","year":"2007","unstructured":"Zalta, E., Fitelson, B.: Steps toward a computational metaphysics. Australas. J. Philos. 36(2), 227\u2013247 (2007)","journal-title":"Australas. J. Philos."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:50Z","timestamp":1750533890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}