{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:12Z","timestamp":1725490872207},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_37","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"508-513","source":"Crossref","is-referenced-by-count":13,"title":["System Description: E- KRHyper"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Pelzer","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","unstructured":"Baumgartner, P., Furbach, U., Pelzer, B.: Hyper Tableau with Equality. In: Fachberichte Informatik 12\u20132007, Universit\u00e4t Koblenz-Landau (2007)"},{"key":"37_CR2","first-page":"352","volume-title":"Automated Deduction \u2013 A Basis for Applications","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Chapter 11: Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2013 A Basis for Applications, vol.\u00a0I, pp. 352\u2013397. Kluwer, Dordrecht (1998)"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (1996)"},{"key":"37_CR4","unstructured":"Wernhard, C.: System Description: KRHyper. In: Fachberichte Informatik 14-2003, Universit\u00e4t Koblenz Landau (2003)"},{"key":"37_CR5","series-title":"Lecture Notes in Artificial Intelligence","first-page":"255","volume-title":"Mechanizing Mathematical Reasoning","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Furbach, U.: Living Books, Automated Deduction and other Strange Things. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol.\u00a02605, pp. 255\u2013274. Springer, Heidelberg (2005)"},{"issue":"3","key":"37_CR6","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., Furbach, U., Gross-Hardt, M., Sinner, A.: Living Book: deduction, slicing, and interaction. J. of Autom. Reasoning\u00a032(3), 259\u2013286 (2004)","journal-title":"J. of Autom. Reasoning"},{"key":"37_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Furbach, U., Gross-Hardt, M., Kleemann, T., Wernhard, C.: KRHyper Inside - Model Based Deduction in Applications. In: Baader, F. (ed.) Automated Deduction \u2013 CADE-19. LNCS (LNAI), vol.\u00a02741, Springer, Heidelberg (2003)"},{"key":"37_CR8","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., Furbach, U., Gross-Hardtand, M., Kleemann, T.: 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)"},{"key":"37_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1007\/978-3-540-30227-8_49","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., Burchardt, A.: Logic Programming Infrastructure for Inferences on FrameNet. In: Alferes, J.J., Leite, J.A. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 591\u2013603. Springer, Heidelberg (2004)"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11853107_2","volume-title":"Principles and Practice of Semantic Web Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Suchanek, F.M.: Automated Reasoning Support for First-Order Ontologies. In: Alferes, J.J., Bailey, J., May, W., Schwertel, U. (eds.) PPSWR 2006. LNCS, vol.\u00a04187, pp. 18\u201332. Springer, Heidelberg (2006)"},{"key":"37_CR11","unstructured":"Baumgartner, P., Mediratta, A.: Improving Stable Models Based Planning by Bidirectional Search. In: International Conference on Knowledge Based Computer Systems (KBCS), Hyderabad, India (2004)"},{"key":"37_CR12","series-title":"Lecture Notes in Artificial Intelligence","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.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"37_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.: Blocking and Other Enhancements of Bottom-Up Model Generation Methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Deransart, P., et al.: Prolog: The standard: reference manual. Berlin (1996)","DOI":"10.1007\/978-3-642-61411-8"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"37_CR16","unstructured":"Ullman, J.D.: Principles of Database and Knowledge-Base Bystems, Rockville, Maryland (1989)"},{"key":"37_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E.R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"37_CR18","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining Superposition, Sorts and Splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"37_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/3-540-61511-3_105","volume-title":"Automated Deduction - Cade-13","author":"H. Sch\u00fctz","year":"1996","unstructured":"Sch\u00fctz, H., Geisler, T.: Efficient model generation through compilation. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol.\u00a01104, pp. 433\u2013447. Springer, Heidelberg (1996)"},{"key":"37_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0027401","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Hasegawa","year":"1997","unstructured":"Hasegawa, R., Fujita, H., Koshimura, M.: MGTP: A Model Generation Theorem Prover \u2014 its advanced features and applications. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol.\u00a01227, pp. 1\u201315. Springer, Heidelberg (1997)"},{"key":"37_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H. Nivelle de","year":"2006","unstructured":"de Nivelle, H., Meng, J.: Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 303\u2013317. Springer, Heidelberg (2006)"},{"key":"37_CR22","doi-asserted-by":"crossref","unstructured":"Niemel\u00e4, I., Simons, P.: Smodels \u2013 An implementation of the stable model and well-founded semantics for normal logic programs. In: Dix, J., Furbach, U., Nerode, A. (eds.) Proc. of the 4th Int. Conf. on Logic Programming and Non-Monotonic Reasoning, pp. 420\u2013429 (1997)","DOI":"10.1007\/3-540-63255-7_32"},{"key":"37_CR23","unstructured":"Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Koch, C., Mateis, C., Perri, S., Scarcello, F.: The DLV System for Knowledge Representation and Reasoning. INFSYS RR-1843-02-14, Technische Universit\u00e4t Wien (2002)"},{"issue":"1","key":"37_CR24","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"key":"37_CR25","unstructured":"McCune, W.: OTTER 3.3 Reference Manual. Argonne National Laboratory, Argonne, Illinois, ANL\/MCS-TM-263 (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:10Z","timestamp":1619517190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}