{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:55:32Z","timestamp":1725512132054},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540699118"},{"type":"electronic","value":"9783540699125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69912-5_14","type":"book-chapter","created":{"date-parts":[[2007,8,20]],"date-time":"2007-08-20T17:30:41Z","timestamp":1187631041000},"page":"174-187","source":"Crossref","is-referenced-by-count":2,"title":["Applications of Automated Reasoning"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Furbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudia","family":"Obermaier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/3-540-45923-5_23","volume-title":"Fundamental Approaches to Software Engineering","author":"W. Ahrendt","year":"2002","unstructured":"Ahrendt, W., et al.: The KeY System: Integrating Object-Oriented Design and Formal Methods. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol.\u00a02306, pp. 327\u2013330. Springer, Heidelberg (2002)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","key":"14_CR2","unstructured":"Baader, F., et al. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"14_CR3","volume-title":"Logic Programming - Proceedings of the 1997 International Symposium","author":"P. Baumgartner","year":"1997","unstructured":"Baumgartner, P., Furbach, U.: Calculi for Disjunctive Logic Programming. In: Maluszynski, J. (ed.) Logic Programming - Proceedings of the 1997 International Symposium, New York, The MIT Press, Cambridge (1997)"},{"key":"14_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-30221-6_14","volume-title":"KI 2004: Advances in Artificial Intelligence","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., et al.: Model Based Deduction for Database Schema Reasoning. In: Biundo, S., Fr\u00fchwirth, T., Palm, G. (eds.) KI 2004. LNCS (LNAI), vol.\u00a03238, pp. 168\u2013182. Springer, Heidelberg (2004)"},{"issue":"3","key":"14_CR5","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1023\/B:JARS.0000044872.51237.c9","volume":"32","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., et al.: Living Book - Deduction, Slicing, and Interaction. J. Autom. Reasoning\u00a032(3), 259\u2013286 (2004)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","first-page":"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)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/3-540-61511-3_95","volume-title":"Automated Deduction - Cade-13","author":"B. Beckert","year":"1996","unstructured":"Beckert, B., et al.: The Tableau-based Theorem Prover \n                    \n                      \n                    \n                    $_{\\mbox{3}}$\n                  T\n                    \n                      \n                    \n                    $^{\\mbox{A}}$\n                  P Version 4.0. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 303\u2013307. Springer, Heidelberg (1996)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Darwiche, A.: Decomposable Negation Normal Form. Journal of the ACM\u00a048(4) (2001), \n                    \n                      citeseer.ist.psu.edu\/477720.html","DOI":"10.1145\/502090.502091"},{"key":"14_CR10","unstructured":"Darwiche, A.: New Advances in Compiling CNF into Decomposable Negation Normal Form. In: Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI\u20192004, pp. 328\u2013332 (2004)"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"1241","DOI":"10.1016\/B978-044450813-3\/50021-7","volume-title":"Handbook of Automated Reasoning","author":"J. Dix","year":"2001","unstructured":"Dix, J., Furbach, U., Niemel\u00e4, I.: Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1241\u20131354. Elsevier, Amsterdam (2001)"},{"key":"14_CR12","unstructured":"Furbach, U., et al.: Issues Management: Erkennen und Beherrschen von kommunikativen Risiken und Chancen. Fachberichte Informatik 2\u20132004, Universit\u00e4t Koblenz-Landau, Institut f\u00fcr Informatik, Koblenz (2004)"},{"issue":"1-2","key":"14_CR13","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/S0004-3702(03)00011-0","volume":"145","author":"U. Furbach","year":"2003","unstructured":"Furbach, U.: AI \u2013 A Multiple Book Review. Artificial Intelligence\u00a0145(1-2), 245 (2003)","journal-title":"Artificial Intelligence"},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/LICS.1996.561342","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science (LICS 1996)","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The Theory of Hybrid Automata. In: Proceedings of the IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 278\u2013292. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"14_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/3-540-45620-1_38","volume-title":"Automated Deduction - CADE-18","author":"T. Hillenbrand","year":"2002","unstructured":"Hillenbrand, T., L\u00f6chner, B.: The Next WALDMEISTER Loop. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 486\u2013500. Springer, Heidelberg (2002)"},{"key":"14_CR16","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":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/11562931_31","volume-title":"Logic Programming","author":"T. Kleemann","year":"2005","unstructured":"Kleemann, T., Sinner, A.: Decision Support for Personalization on Mobile Devices. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 404\u2013406. Springer, Heidelberg (2005)"},{"key":"14_CR18","series-title":"Lecture Notes in Artificial Intelligence","first-page":"452","volume-title":"Automated Deduction \u2013 CADE-20","author":"T. Kleemann","year":"2005","unstructured":"Kleemann, T., Sinner, A.: Krhyper - in your Pocket, System Description. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 452\u2013458. Springer, Heidelberg (2005)"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Loveland, D.: Mechanical Theorem Proving by Model Elimination. JACM\u00a015(2) (1968)","DOI":"10.1145\/321450.321456"},{"key":"14_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-48754-9_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"F. Massacci","year":"1999","unstructured":"Massacci, F.: Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 14\u201318. Springer, Heidelberg (1999)"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"10th International Conference on Automated Deduction","author":"W. McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 663\u2013664. Springer, Heidelberg (1990)"},{"issue":"3","key":"14_CR22","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. J. Autom. Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR23","volume-title":"Computational Intelligence: A Logical Approach","author":"D. Poole","year":"1997","unstructured":"Poole, D., Mackworth, A., Goebel, R.: Computational Intelligence: A Logical Approach. Oxford University Press, Oxford (1997)"},{"issue":"2-3","key":"14_CR24","first-page":"79","volume":"15","author":"F. Pelletier","year":"2002","unstructured":"Pelletier, F., Sutcliffe, G., Suttner, C.: The Development of CASC. AI Communications\u00a015(2-3), 79\u201390 (2002)","journal-title":"AI Communications"},{"key":"14_CR25","volume-title":"Handbook of Automated Reasoning","author":"J.A. Robinson","year":"2001","unstructured":"Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning (in 2 volumes). Elsevier, Amsterdam (2001)"},{"issue":"2-3","key":"14_CR26","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"14_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"issue":"2","key":"14_CR28","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"14_CR29","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: Spass - version 0.49. Journal of Automated Reasoning\u00a018(2), 247\u2013252 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR30","unstructured":"Wernhard, C.: System Description: KRHyper. Fachberichte Informatik 14\u20132003, Universit\u00e4t Koblenz-Landau, Institut f\u00fcr Informatik, Koblenz (2003)"},{"key":"14_CR31","unstructured":"Wernhard, C.: Tableaux Between Proving, Projection and Compilation. Technical report, Universit\u00e4t Koblenz-Landau. In preparation (2006)"}],"container-title":["Lecture Notes in Computer Science","KI 2006: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69912-5_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:11:55Z","timestamp":1620000715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69912-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540699118","9783540699125"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69912-5_14","relation":{},"subject":[]}}