{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T19:32:17Z","timestamp":1649187137142},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2010,8,6]],"date-time":"2010-08-06T00:00:00Z","timestamp":1281052800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Informatik Spektrum"],"published-print":{"date-parts":[[2010,10]]},"DOI":"10.1007\/s00287-010-0461-3","type":"journal-article","created":{"date-parts":[[2010,8,5]],"date-time":"2010-08-05T09:02:28Z","timestamp":1280998948000},"page":"444-451","source":"Crossref","is-referenced-by-count":1,"title":["Deduktion: von der Theorie zur Anwendung"],"prefix":"10.1007","volume":"33","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Beckert","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,8,6]]},"reference":[{"key":"461_CR1","doi-asserted-by":"crossref","unstructured":"Alkassar E, Hillebrand M, Leinenbach D, Schirmer N, Starostin A (2008) The Verisoft approach to systems verification. In: Shankar N, Woodcock J (eds) Verified Software: Theories, Tools, Experiments (VSTTE 2008), vol 5295 of LNCS. Springer, pp 209\u2013224","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"461_CR2","doi-asserted-by":"crossref","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K Appel","year":"1976","unstructured":"Appel K, Haken W (1976) Every planar map is four colorable. Bull AMS 82:711\u2013712","journal-title":"Bull AMS"},{"key":"461_CR3","doi-asserted-by":"crossref","unstructured":"Baader F, Nipkow T (1998) Term Rewriting and All That. Cambridge University Press, Cambridge, UK","DOI":"10.1017\/CBO9781139172752"},{"key":"461_CR4","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F Baader","year":"2001","unstructured":"Baader F, Sattler U (2001) An overview of tableau algorithms for description logics. Stud Logica 69:5\u201340","journal-title":"Stud Logica"},{"key":"461_CR5","unstructured":"Baader F, Calvanese D, McGuinness D, Nardi D, Patel-Schneider PF (eds) (2003) The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge, UK"},{"key":"461_CR6","doi-asserted-by":"crossref","unstructured":"Barrett C, Tinelli C (2007) CVC3. In: Damm W, Hermanns H (eds) Proceedings, 19th International Conference on Computer Aided Verification (CAV \u201907), LNCS 4590. Springer, pp 298\u2013302","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"461_CR7","doi-asserted-by":"crossref","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive Theorem Proving and Program Development. Springer, Berlin, Deutschland","DOI":"10.1007\/978-3-662-07964-5"},{"key":"461_CR8","unstructured":"Claessen K, S\u00f6rensson N (2003) New techniques that improve MACE-style finite model finding. In: Baumgartner P, Ferm\u00fcller C (eds) Proceedings of the CADE-19 Workshop: Model Computation \u2013 Principles, Algorithms, Applications (Miami, USA)"},{"issue":"2","key":"461_CR9","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1006\/jabr.1998.7467","volume":"208","author":"BI Dahn","year":"1998","unstructured":"Dahn BI (1998) Robbins algebras are boolean: A revision of mccune\u2019s computer-generated solution of Robbins\u2019s problem. J Algebra 208(2):526\u2013532","journal-title":"J Algebra"},{"key":"461_CR10","unstructured":"Dutertre B (2007) System description: Yices 1.0.10. In: SMT-COMP\u201907"},{"key":"461_CR11","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier G (2008) Formal proof \u2013 the four-color theorem. Not AMS 55:1382\u20131393","journal-title":"Not AMS"},{"key":"461_CR12","first-page":"440","volume":"47","author":"TC Hales","year":"2000","unstructured":"Hales TC (2000) Cannonballs and honeycombs. Not AMS 47:440\u2013449","journal-title":"Not AMS"},{"key":"461_CR13","doi-asserted-by":"crossref","unstructured":"Hales TC, Harrison J, McLaughlin S, Nipkow T, Obua S, Zumkeller R (2009) A revision of the proof of the Kepler conjecture. Discr Comput Geom, Published online","DOI":"10.1007\/s00454-009-9148-4"},{"key":"461_CR14","unstructured":"van Harmelen F, Lifschitz V, Porter B (eds) (2007) Handbook of Knowledge Representation (Foundations of Artificial Intelligence). Elsevier Science, San Diego, USA"},{"key":"461_CR15","doi-asserted-by":"crossref","unstructured":"Harrison J (2009) HOL Light: An overview. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of LNCS. Springer, pp 60\u201366","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"461_CR16","doi-asserted-by":"crossref","unstructured":"Hillenbrand T (2003) Citius altius fortius: Lessons learned from the theorem prover WALDMEISTER. Electr Notes Theor Comput Sci 86(1):13","DOI":"10.1016\/S1571-0661(04)80649-2"},{"key":"461_CR17","unstructured":"Horrocks I (2003) Implementation and optimization techniques. In: Baader F, Calvanese D, McGuinness D, Nardi D, Patel-Schneider PF (eds) The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, pp 306\u2013346"},{"key":"461_CR18","unstructured":"Horrocks I, Sattler U (2005) A tableaux decision procedure for SHOIQ. In: Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI 2005), Edinburgh (UK). Morgan Kaufmann"},{"key":"461_CR19","unstructured":"Horrocks I, Kutz O, Sattler U (2006) The even more irresistible SROIQ. In: Doherty P, Mylopoulos J, Welty CA (eds) Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006), Lake District, UK, 2006. AAAI Press\/The MIT Press, pp 57\u201367"},{"key":"461_CR20","doi-asserted-by":"crossref","unstructured":"Hustadt U, Schmidt R (2000) MSPASS: Modal reasoning by translation and first-order resolution. In: Dyckhoff R (ed) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference (TABLEAUX 2000), vol 1847 of Lecture Notes in Artificial Intelligence, Springer, pp 67\u201371","DOI":"10.1007\/10722086_7"},{"key":"461_CR21","unstructured":"Hustadt U, Motik B, Sattler U (2004) Reducing SHIQ-description logic to disjunctive datalog programs. In: Dubois D, Welty CA, Williams M-A (eds) Proc. of the 9th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2004). Morgan Kaufmann, pp 152\u2013162"},{"key":"461_CR22","doi-asserted-by":"crossref","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"461_CR23","doi-asserted-by":"crossref","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: Formal verification of an OS kernel. In: Proc. 22nd ACM Symposium on Operating Systems Principles (SOSP). ACM, pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"461_CR24","doi-asserted-by":"crossref","unstructured":"Loveland DE (2000) Automated deduction: Achievements and future directions. Commun ACM 43(11)","DOI":"10.1145\/352515.352529"},{"key":"461_CR25","doi-asserted-by":"crossref","unstructured":"McLaughlin S, Harrison J (2005) A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis R (ed) Automated Deduction (CADE-20), volume 3632 of LNCS. Springer, pp 295\u2013314","DOI":"10.1007\/11532231_22"},{"key":"461_CR26","doi-asserted-by":"crossref","unstructured":"Minker J (ed) (2000) Logic-Based Artificial Intelligence. Kluwer Academic Publisher","DOI":"10.1007\/978-1-4615-1567-8"},{"key":"461_CR27","unstructured":"Minsky M (1981) A framework for representing knowledge. In: Haugeland J (ed) Mind Design. The MIT Press, Cambridge, USA. A longer version appeared in The Psychology of Computer Vision (1975)"},{"key":"461_CR28","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 14th International Conference, Budapest, Hungary, LNCS 4963. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"461_CR29","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0004-3702(90)90087-G","volume":"43","author":"B Nebel","year":"1990","unstructured":"Nebel B (1990) Terminological reasoning is inherently intractable. Artif Intel 43:235\u2013249","journal-title":"Artif Intel"},{"key":"461_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson L, Wenzel M (2002) Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer","DOI":"10.1007\/3-540-45949-9"},{"key":"461_CR31","doi-asserted-by":"crossref","unstructured":"Nipkow T, Bauer G, Schultz P (2006) Flyspeck I: Tame graphs. In: Furbach U, Shankar N (eds) Automated Reasoning (IJCAR 2006), volume 4130 of LNCS. Springer, pp 21\u201335","DOI":"10.1007\/11814771_4"},{"key":"461_CR32","doi-asserted-by":"crossref","unstructured":"Owre S, Shankar N (2008) A brief overview of PVS. In: Mohamed OA, Mu\u00f1oz C, Tahar S (eds) Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS. Springer, pp 22\u201327","DOI":"10.1007\/978-3-540-71067-7_5"},{"key":"461_CR33","unstructured":"Quillian MR (1968) Semantic memory. In: Minsky M (ed) Semantic Information Processing. The MIT Press, pp 216\u2013270"},{"key":"461_CR34","unstructured":"Ranise S, Tinelli C (2006) The SMT-LIB standard: Version 1.2. Technical report. Department of Computer Science, The University of Iowa"},{"issue":"2\u20133","key":"461_CR35","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov A, Voronkov A (2002) The design and implementation of VAMPIRE. AI Commun 15(2\u20133):91\u2013110","journal-title":"AI Commun"},{"issue":"1","key":"461_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M Schmidt-Schau\u00df","year":"1991","unstructured":"Schmidt-Schau\u00df M, Smolka G (1991) Attributive concept descriptions with complements. Artif Intel 48(1):1\u201326","journal-title":"Artif Intel"},{"key":"461_CR37","doi-asserted-by":"crossref","unstructured":"Schulz S (2004) System description: E 0.81. In: Basin DA, Rusinowitch M (eds) Automated Reasoning \u2013 Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4\u20138, 2004, Proceedings, LNCS 3097. Springer, pp 223\u2013228","DOI":"10.1007\/978-3-540-25984-8_15"},{"key":"461_CR38","doi-asserted-by":"crossref","unstructured":"Slind K, Norrish M (2008) A brief overview of HOL4. In: Mohamed OA, Mu\u00f1oz C, Tahar S (eds) Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS. Springer, pp 28\u201332","DOI":"10.1007\/978-3-540-71067-7_6"},{"issue":"1","key":"461_CR39","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe G (2009) The 4th IJCAR automated theorem proving system competition \u2013 CASC-J4. AI Commun 22(1):59\u201372","journal-title":"AI Commun"},{"key":"461_CR40","unstructured":"Sutcliffe G, Suttner C, The TPTP problem library for automated theorem proving. At http:\/\/www.cs.miami.edu\/\u223ctptp\/, letzter Zugriff 3.8.2010"},{"key":"461_CR41","unstructured":"Winwood S, Klein G, Sewell T, Andronick J, Cock D, Norrish M (2009) Mind the gap: A verification framework for low-level C. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of LNCS. Springer, pp 500\u2013515"}],"container-title":["Informatik-Spektrum"],"original-title":[],"language":"de","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00287-010-0461-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00287-010-0461-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00287-010-0461-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,10]],"date-time":"2020-06-10T01:43:32Z","timestamp":1591753412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00287-010-0461-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,8,6]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,10]]}},"alternative-id":["461"],"URL":"https:\/\/doi.org\/10.1007\/s00287-010-0461-3","relation":{},"ISSN":["0170-6012","1432-122X"],"issn-type":[{"value":"0170-6012","type":"print"},{"value":"1432-122X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8,6]]}}}