{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:45:03Z","timestamp":1743029103243,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642034282"},{"type":"electronic","value":"9783642034299"}],"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-03429-9_21","type":"book-chapter","created":{"date-parts":[[2009,8,28]],"date-time":"2009-08-28T08:12:52Z","timestamp":1251447172000},"page":"326-341","source":"Crossref","is-referenced-by-count":0,"title":["Translating a Dependently-Typed Logic to First-Order Logic"],"prefix":"10.1007","author":[{"given":"Kristina","family":"Sojakova","sequence":"first","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science (2002)","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"21_CR2","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"Proceedings of the 14th Conference on Automated Deduction","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Melis, E., Meier, A., Schaarschmidt, W., Siekmann, J., Sorge, V.: \u03a9MEGA: Towards a mathematical assistant. In: McCune, W. (ed.) Proceedings of the 14th Conference on Automated Deduction, pp. 252\u2013255. Springer, Heidelberg (1997)"},{"key":"21_CR3","first-page":"33","volume-title":"TYPES 2008","author":"J. Belo","year":"2008","unstructured":"Belo, J.: Dependently Sorted Logic. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2008, pp. 33\u201350. Springer, Heidelberg (2008)"},{"key":"21_CR4","unstructured":"Benzmller, C., Paulson, L., Theiss, F., Fietzke, A.: The LEO-II Project. In: Automated Reasoning Workshop (2007)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/11814771_19","volume-title":"Automated Reasoning","author":"C. Brown","year":"2006","unstructured":"Brown, C.: Combining Type Theory and Untyped Set Theory. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 205\u2013219. Springer, Heidelberg (2006)"},{"key":"21_CR6","first-page":"342","volume-title":"Mathematical Foundations of Computer Science","author":"M. Cerioli","year":"1993","unstructured":"Cerioli, M., Meseguer, J.: May I Borrow Your Logic? In: Borzyszkowski, A., Sokolowski, S. (eds.) Mathematical Foundations of Computer Science, pp. 342\u2013351. Springer, Heidelberg (1993)"},{"key":"21_CR7","unstructured":"Claessen, K., Sorensson, N.: New techniques that improve MACE-style finite model finding. In: 19th International Conference on Automated Deduction (CADE-19) Workshop on Model Computation - Principles, Algorithms, Applications (2003)"},{"issue":"1","key":"21_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. Goguen","year":"1992","unstructured":"Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery\u00a039(1), 95\u2013146 (1992)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"21_CR9","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J. (ed.) Applications of Algebraic Specification using OBJ, Cambridge (1993)"},{"issue":"1","key":"21_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Melham, T.: Translating dependent type theory into higher order logic. In: Bezem, M., Groote, J. (eds.) Typed Lambda Calculi and Applications, pp. 209\u2013229 (1993)","DOI":"10.1007\/BFb0037108"},{"key":"21_CR12","volume-title":"Categories for the Working Mathematician","author":"S. Mac Lane","year":"1998","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1998)"},{"key":"21_CR13","unstructured":"Makkai, M.: First order logic with dependent sorts, FOLDS (1997) (Unpublished)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the Logic Colloquium 1973, pp. 73\u2013118 (1975)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"key":"21_CR16","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press, Oxford (1990)"},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF01396685","volume":"145","author":"A. Oberschelp","year":"1962","unstructured":"Oberschelp, A.: Untersuchungen zur mehrsortigen Quantorenlogik. Mathematische Annalen\u00a0145, 297\u2013333 (1962)","journal-title":"Mathematische Annalen"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"21_CR19","series-title":"Algebraic and Logical Structures","first-page":"39","volume-title":"Handbook of Logic in Computer Science ch. 2","author":"A. Pitts","year":"2000","unstructured":"Pitts, A.: Categorical Logic. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science ch. 2. Algebraic and Logical Structures, vol.\u00a05, pp. 39\u2013128. Oxford University Press, Oxford (2000)"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/11814771_33","volume-title":"Automated Reasoning","author":"F. Rabe","year":"2006","unstructured":"Rabe, F.: First-Order Logic with Dependent Types. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol.\u00a04130, pp. 377\u2013391. Springer, Heidelberg (2006)"},{"key":"21_CR21","unstructured":"Rabe, F.: Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen (2008)"},{"key":"21_CR22","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015, 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"21_CR23","unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with Mizar. In: Proceedings of the 9th International Joint Conference on Artificial Intelligence, Los Angeles, CA, pp. 26\u201328 (1985)"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2003","unstructured":"Urban, J.: Translating Mizar for first-order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 203\u2013215. Springer, Heidelberg (2003)"},{"key":"21_CR25","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE-16)","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topi\u0107, D.: System description: SPASS version 1.0.0. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE-16). LNCS (LNAI), vol.\u00a01632, pp. 314\u2013318. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03429-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T03:45:48Z","timestamp":1558496748000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03429-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642034282","9783642034299"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03429-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}