{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:38:08Z","timestamp":1725536288897},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_13","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"164-179","source":"Crossref","is-referenced-by-count":5,"title":["Extended First-Order Logic"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[]},{"given":"Gert","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning","author":"P.B. Andrews","year":"2001","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, pp. 965\u20131007. Elsevier Science, Amsterdam (2001)"},{"key":"13_CR2","unstructured":"Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church\u2019s Type Theory. College Publications (2007)"},{"key":"13_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"13_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)"},{"key":"13_CR5","doi-asserted-by":"publisher","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. Springer, Heidelberg (1996)"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"452","DOI":"10.2307\/2270331","volume":"33","author":"D. Prawitz","year":"1968","unstructured":"Prawitz, D.: Hauptsatz for higher order logic. J. Symb. Log.\u00a033, 452\u2013457 (1968)","journal-title":"J. Symb. Log."},{"key":"13_CR7","series-title":"LNCS (LNAI)","first-page":"138","volume-title":"TABLEAUX 2009","author":"C.E. Brown","year":"2009","unstructured":"Brown, C.E., Smolka, G.: Terminating tableaux for the basic fragment of simple type theory. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol.\u00a05607, pp. 138\u2013151. Springer, Heidelberg (2009)"},{"key":"13_CR8","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511608865","volume-title":"Basic Simple Type Theory","author":"J.R. Hindley","year":"1997","unstructured":"Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol.\u00a042. Cambridge University Press, Cambridge (1997)"},{"key":"13_CR9","series-title":"Lectures Notes in Mathematics","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/BFb0064870","volume-title":"Proc. Logic Colloquium 1972-73","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Proc. Logic Colloquium 1972-73. Lectures Notes in Mathematics, vol.\u00a0453, pp. 22\u201337. Springer, Heidelberg (1975)"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"17","DOI":"10.2307\/2273377","volume":"47","author":"R. Statman","year":"1982","unstructured":"Statman, R.: Completeness, invariance and lambda-definability. J. Symb. Log.\u00a047(1), 17\u201326 (1982)","journal-title":"J. Symb. Log."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:24:29Z","timestamp":1552119869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}