{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:28Z","timestamp":1725728968025},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_8","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"126-134","source":"Crossref","is-referenced-by-count":15,"title":["System Description: E-KRHyper 1.4"],"prefix":"10.1007","author":[{"given":"Markus","family":"Bender","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bj\u00f6rn","family":"Pelzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudia","family":"Schon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/B978-0-934613-40-8.50006-3","volume-title":"Foundations of Deductive Databases and Logic Programming","author":"K.R. Apt","year":"1988","unstructured":"Apt, K.R., Blair, H.A., Walker, A.: Towards a theory of declarative knowledge. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 89\u2013148. Morgan Kaufmann Publishers Inc., San Francisco (1988)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. (2009)","DOI":"10.1145\/1459010.1459014"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Resolution-based theorem proving for manyvalued logics. J. Symb. Comput. (1995)","DOI":"10.1006\/jsco.1995.1021"},{"key":"8_CR4","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2014 A Basis for Applications. Kluwer (1998)"},{"key":"8_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 591\u2013603. Springer, Heidelberg (2004)"},{"key":"8_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-32254-2_15","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. 249\u2013267. Springer, Heidelberg (2005)"},{"key":"8_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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-Hardt, 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":"8_CR8","unstructured":"Baumgartner, P., Furbach, U., Gross-Hardt, M., Kleemann, T., Wernhard, C.: KRHyper inside - model based deduction in applications. Fachberichte informatik, Universit\u00e4t Koblenz-Landau (2003)"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Gro\u00df-Hardt, M., Sinner, A.: Living book - deduction, slicing, and interaction. J. Autom. Reason (2004)","DOI":"10.1007\/s10817-004-2041-1"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Koblenz, U.: PROTEIN: A PROver with a Theory Extension INterface. In: CADE-12, Proc. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58156-1_57"},{"key":"8_CR11","doi-asserted-by":"crossref","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)","DOI":"10.1007\/3-540-61630-6_1"},{"key":"8_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-540-73595-3_36","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. Baumgartner","year":"2007","unstructured":"Baumgartner, P., Furbach, U., Pelzer, B.: Hyper tableaux with equality. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 492\u2013507. Springer, Heidelberg (2007)"},{"key":"8_CR13","unstructured":"Baumgartner, P., Mediratta, A.: Improving stable models-based planning by bidirectional search. In: International Conference on Knowledge Based Computer Systems (KBCS) (December 2004)"},{"key":"8_CR14","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":"8_CR15","unstructured":"Bender, M.: E-hyper tableaux with distinct object identifiers. Arbeitsberichte aus dem Fachbereich Informatik 01\/2013, Universit\u00e4t Koblenz-Landau (2013), \n                  \n                    http:\/\/www.uni-koblenz.de\/FB4\/Publications\/Reports"},{"key":"8_CR16","unstructured":"Fa\u00dfbender, D.: DLE-hyper tableau calculus. Diplomarbeit, University of Koblenz-Landau (February 2012)"},{"key":"8_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-71070-7_11","volume-title":"Automated Reasoning","author":"U. Furbach","year":"2008","unstructured":"Furbach, U., Gl\u00f6ckner, I., Helbig, H., Pelzer, B.: Loganswer - a deduction-based question answering system (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 139\u2013146. Springer, Heidelberg (2008)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Furbach, U., Gl\u00f6ckner, I., Helbig, H., Pelzer, B.: Logic-based question answering. In: KI (2010)","DOI":"10.1007\/s13218-010-0010-x"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Furbach, U., Gl\u00f6ckner, I., Pelzer, B.: An application of automated reasoning in natural language question answering. In: AI Commun. (2010) (PAAR Special Issue)","DOI":"10.3233\/AIC-2010-0461"},{"key":"8_CR20","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V.: Chaining techniques for automated theorem proving in many-valued logics. In: Proc. ISMVL 2000. IEEE Computer Society (2000)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","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, vol.\u00a06803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"8_CR22","unstructured":"Horrocks, I.: Header Benchmarks (2009-2013), \n                  \n                    http:\/\/hermit-reasoner.com\/2009\/JAIR_benchmarks\/\n                  \n                  \n                 (accessed January 9, 2013)"},{"key":"8_CR23","unstructured":"Horrocks, I., Fensel, D., Broekstra, J., Decker, S., Erdmann, M., Goble, C., van Harmelen, F., Klein, M., Staab, S., Studer, R., Motta, E.: Oil: The ontology inference layer. Technical report, Vrije Universiteit Amsterdam, Faculty of Sciences (September 2000), \n                  \n                    http:\/\/www.ontoknowledge.org\/oil\/"},{"key":"8_CR24","unstructured":"INRIA. Objective Caml (OCaml) programming language website, \n                  \n                    http:\/\/ocaml.org\/"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.3 Reference Manual. Argonne National Laboratory (2003)","DOI":"10.2172\/822573"},{"key":"8_CR26","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set (hets). In: Beckert, B. (ed.) VERIFY. CEUR Workshop Proceedings, vol.\u00a0259. CEUR-WS.org (2007)"},{"key":"8_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-73595-3_6","volume-title":"Automated Deduction \u2013 CADE-21","author":"B. Motik","year":"2007","unstructured":"Motik, B., Shearer, R., Horrocks, I.: Optimized reasoning in description logics using hypertableaux. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 67\u201383. Springer, Heidelberg (2007)"},{"key":"8_CR28","unstructured":"Parsia, B., Sirin, E.: Pellet: An owl dl reasoner. In: 3rd International Semantic Web Conference (ISWC 2004) (2004)"},{"key":"8_CR29","unstructured":"Pelzer, B.: Project website of E-KRHyper (2007-2013), \n                  \n                    http:\/\/userp.uni-koblenz.de\/~bpelzer\/ekrhyper\/\n                  \n                  \n                 (accessed January 21, 2013)"},{"key":"8_CR30","unstructured":"Pelzer, B., Gl\u00f6ckner, I.: Combining theorem proving with natural language processing. In: Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning (PAAR-2008\/ESHOL-2008), Sydney, Australia, August 10-11. CEUR Workshop Proceedings (2008)"},{"key":"8_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-540-73595-3_37","volume-title":"Automated Deduction \u2013 CADE-21","author":"B. Pelzer","year":"2007","unstructured":"Pelzer, B., Wernhard, C.: System description: E- kRHyper. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 508\u2013513. Springer, Heidelberg (2007)"},{"key":"8_CR32","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Commun. (2002)"},{"key":"8_CR33","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. (2002)"},{"key":"8_CR34","unstructured":"Schulz, S., Bonacina, M.P.: On handling distinct objects in the superposition calculus. In: Konev, B., Schulz, S. (eds.) Proc. IWIL (2005)"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-14418-9_3","volume-title":"Controlled Natural Language","author":"R. Schwitter","year":"2010","unstructured":"Schwitter, R.: Anaphora resolution involving interactive knowledge acquisition. In: Fuchs, N.E. (ed.) CNL 2009. LNCS, vol.\u00a05972, pp. 36\u201355. Springer, Heidelberg (2010)"},{"key":"8_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11532231_33","volume-title":"Automated Deduction \u2013 CADE-20","author":"A. Sinner","year":"2005","unstructured":"Sinner, A., Kleemann, T.: KRHyper - In Your Pocket. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 452\u2013457. Springer, Heidelberg (2005)"},{"key":"8_CR37","unstructured":"Sutcliffe, G.: The TPTP website (2004-2013), \n                  \n                    http:\/\/www.tptp.org\n                  \n                  \n                 (accessed January 21, 2013)"},{"key":"8_CR38","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reason. (2009)"},{"key":"8_CR39","unstructured":"Wernhard, C.: System description: KRHyper. Fachberichte informatik, Universit\u00e4t Koblenz-Landau (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T16:09:16Z","timestamp":1578499756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_8"}},"subtitle":["Extensions for Unique Names and Description Logic"],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}