{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:38Z","timestamp":1725474518888},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540650805"},{"type":"electronic","value":"9783540496564"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0095435","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:28:18Z","timestamp":1164378498000},"page":"141-152","source":"Crossref","is-referenced-by-count":1,"title":["Simultaneous quantifier elimination"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heiko","family":"Mantel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Werner","family":"Stephan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,20]]},"reference":[{"key":"13_CR1","unstructured":"S. Autexier and H. Mantel. Semantical Investigation of Simultaneous Skolemization for First-Order Sequent Calculus, Seki Report SR-98-05, 1998."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"A. Avron. Simple Consequence Relations, In Information and Computation 92, p. 105\u2013139, 1991.","DOI":"10.1016\/0890-5401(91)90023-U"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 2nd edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"13_CR4","unstructured":"K. A. Bowen. Programming with full first-order logic, In Hayes, Michie, Pao, Eds., Machine Intelligence 10, 1982."},{"key":"13_CR5","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar and M. Srivas. A Tutorial Introduction to PVS, Presented at WIFT\u201995, 1995."},{"key":"13_CR6","first-page":"179","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u00dfen, Mathematische Zeitschrift. 39:179\u2013210 and 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"D. Hutter, B. Langenstein, C. Sengler, J. Siekmann, W. Stephan and A. Wolpers. Verification Support Environment (VSE), High Integrity Systems, p. 523\u2013530, 1996.","DOI":"10.1007\/3-540-60973-3_92"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"J. Ketonen and R. Weyhrauch. A Decidable Fragment of Predicate Calculus, In TCS, Volume 32\u20133, 1984.","DOI":"10.1016\/0304-3975(84)90047-1"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"P. Lincoln and N. Shankar. Proof Search in First-Order Linear Logic and other Cut-Free Sequent Calculi, In Proceedings of 9th LICS, p. 282\u2013291, 1994.","DOI":"10.1109\/LICS.1994.316061"},{"key":"13_CR10","unstructured":"J. Loeckx, H.-D. Ehrich and M. Wolf. Specification of Abstract Data Types, Wiley-Teubner, 1996."},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Isabelle, A Generic Theorem Prover, Springer Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"N. Shankar. Proof Search in the Intuitionistic Sequent Calculus, In D. Kapur, Ed., Proceedings of CADE-11, p. 522\u2013536, 1992.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"13_CR13","unstructured":"T. Skolem. Logisch-kombinatorische Untersuchungen \u00fcber die Erf\u00fcllbarkeit oder Beweisbarkeit mathematischer S\u00e4tze, In Skrifter utgit av Videnskapselskapet i Kristiania, p. 4\u201336, 1920."},{"key":"13_CR14","unstructured":"L. Wallen. Automated Deduction in Non-Classical Logic. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","KI-98: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0095435","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T14:54:31Z","timestamp":1555944871000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0095435"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650805","9783540496564"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0095435","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}