{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:37:54Z","timestamp":1725471474730},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540659228"},{"type":"electronic","value":"9783540488552"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"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":[[1999]]},"DOI":"10.1007\/10703163_7","type":"book-chapter","created":{"date-parts":[[2006,10,9]],"date-time":"2006-10-09T18:15:50Z","timestamp":1160417750000},"page":"90-104","source":"Crossref","is-referenced-by-count":1,"title":["Quantifiers and the System KE: Some Surprising Results"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/978-94-017-0435-9_12","volume-title":"Automated Deduction\u2013 A Basis for Applications, part 4, ch. 12","author":"M. Baaz","year":"1998","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Extension Methods in Automated Deduction. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2013 A Basis for Applications, part 4, ch. 12, vol.\u00a0II, pp. 331\u2013360. Kluwer Academic Press, Dordrecht (1998)"},{"key":"7_CR2","first-page":"213","volume-title":"LICS 1994","author":"M. Baaz","year":"1994","unstructured":"Baaz, M., Ferm\u00fcller, C., Leitsch, A.: A Non-Elementary Speed Up in Proof Length by Structural Clause Form Transformation. In: LICS 1994, pp. 213\u2013219. IEEE Computer Society Press, Los Alamitos (1994)"},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"Baaz, M., Leitsch, A.: On Skolemization and Proof Complexity. Fundamenta Informaticae\u00a020, 353\u2013379 (1994)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"Beckert, B., Posegga, J.: leanTAP: Lean Tableau-based Deduction. J. Automated Reasoning\u00a015(3), 339\u2013358 (1995)","journal-title":"J. Automated Reasoning"},{"key":"7_CR5","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BF00156916","volume":"1","author":"M. D\u2019Agostino","year":"1992","unstructured":"D\u2019Agostino, M.: Are Tableaux an Improvement on Truth-Tables? Cut-Free Proofs and Bivalence. J. Logic, Language and Information\u00a01, 235\u2013252 (1992)","journal-title":"J. Logic, Language and Information"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D\u2019Agostino","year":"1994","unstructured":"D\u2019Agostino, M., Mondadori, M.: The Taming of the Cut. Classical Refutations with Analytic Cut. J. Logic and Computation\u00a04, 285\u2013319 (1994)","journal-title":"J. Logic and Computation"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Eder, E.: Relative Complexities of First Order Calculi. Vieweg (1992)","DOI":"10.1007\/978-3-322-84222-0"},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/3-540-58216-9_30","volume-title":"Proceedings of the International Conference on Logic Programming and Automated Reasoning","author":"U. Egly","year":"1994","unstructured":"Egly, U.: On the Value of Antiprenexing. In: Pfenning, F. (ed.) Proceedings of the International Conference on Logic Programming and Automated Reasoning, pp. 69\u201383. Springer, Heidelberg (1994)"},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1006\/jsco.1996.0044","volume":"22","author":"U. Egly","year":"1996","unstructured":"Egly, U.: On Different Structure-preserving Translations to Normal Form. J. Symbolic Computation\u00a022, 121\u2013142 (1996)","journal-title":"J. Symbolic Computation"},{"key":"7_CR10","first-page":"103","volume-title":"Automated Deduction\u2013 A Basis for Applications, part 1, ch. 4","author":"U. Egly","year":"1998","unstructured":"Egly, U.: Cuts in Tableaux. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2013 A Basis for Applications, part 1, ch. 4, vol.\u00a0I, pp. 103\u2013132. Kluwer Academic Press, Dordrecht (1998)"},{"key":"7_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"7_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)"},{"key":"7_CR13","first-page":"121","volume-title":"Proceedings of IJCAI-1985","author":"V. Lifschitz","year":"1985","unstructured":"Lifschitz, V.: Computing Circumscription. In: Proceedings of IJCAI-1985, Los Altos, CA., pp. 121\u2013127. Morgan Kaufmann, San Francisco (1985)"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"McCarthy, J.: Circumscription \u2013 A Form of Non-Monotonic Reasoning. Artificial Intelligence\u00a013, 27\u201339 (1980)","journal-title":"Artificial Intelligence"},{"key":"7_CR15","unstructured":"Mondadori, M.: Classical Analytical Deduction. Technical Report Annali dell\u2019Universit\u00e0 di Ferrara, Sezione III, Discussion Paper 1, Universit\u00e0 di Ferrara (1988)"},{"key":"7_CR16","first-page":"137","volume":"88","author":"V.P. Orevkov","year":"1979","unstructured":"Orevkov, V.P.: Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR\u00a088, 137\u2013161 (1979); English translation in J. Soviet Mathematics, pp. 2337\u20132350 (1982)","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im V. A. Steklova AN SSSR"},{"key":"7_CR17","unstructured":"Sieg, W., Kauffmann, B.: Unification for Quantified Formulae. PHIL 44, Carnegie Mellon University (1993)"},{"key":"#cr-split#-7_CR18.1","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part II, Leningrad. Seminars in Mathematics, vol.\u00a08, pp. 234-259 (1968)"},{"key":"#cr-split#-7_CR18.2","unstructured":"English translation: Consultants Bureau, New York, pp. 115-125 (1970)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703163_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T13:45:19Z","timestamp":1587217519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703163_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540659228","9783540488552"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/10703163_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}