×

Translating a dependently-typed logic to first-order logic. (English) Zbl 1253.03100

Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 326-341 (2009).
Summary: DFOL is a logic that extends first-order logic with dependent types. We give a translation from DFOL to FOL formalized as an institution comorphism and show that it admits the model expansion property. This property together with the borrowing theorem implies the soundness of borrowing – a result that enables us to reason about entailment in DFOL by using automated tools for FOL. In addition, the translation permits us to deduce properties of DFOL such as completeness, compactness, and existence of free models from the corresponding properties of FOL, and to regard DFOL as a fragment of FOL. We give an example that shows how problems about DFOL can be solved by using the automated FOL prover Vampire. Future work will focus on the integration of the translation into the specification and translation tool HeTS.
For the entire collection see [Zbl 1173.68005].

MSC:

03G30 Categorical logic, topoi
68Q65 Abstract data types; algebraic specification
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science (2002) · Zbl 1061.68103 · doi:10.1016/S0304-3975(01)00368-1
[2] Benzmüller, 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.: {\(\Omega\)}MEGA: Towards a mathematical assistant. In: McCune, W. (ed.) Proceedings of the 14th Conference on Automated Deduction, pp. 252–255. Springer, Heidelberg (1997) · doi:10.1007/3-540-63104-6_23
[3] Belo, J.: Dependently Sorted Logic. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2008, pp. 33–50. Springer, Heidelberg (2008) · Zbl 1139.03020
[4] Benzmller, C., Paulson, L., Theiss, F., Fietzke, A.: The LEO-II Project. In: Automated Reasoning Workshop (2007)
[5] Brown, C.: Combining Type Theory and Untyped Set Theory. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 205–219. Springer, Heidelberg (2006) · Zbl 1222.03012 · doi:10.1007/11814771_19
[6] Cerioli, M., Meseguer, J.: May I Borrow Your Logic? In: Borzyszkowski, A., Sokolowski, S. (eds.) Mathematical Foundations of Computer Science, pp. 342–351. Springer, Heidelberg (1993) · Zbl 0925.03148
[7] 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)
[8] Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992) · Zbl 0799.68134 · doi:10.1145/147508.147524
[9] Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. In: Goguen, J. (ed.) Applications of Algebraic Specification using OBJ, Cambridge (1993)
[10] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060
[11] 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–229 (1993) · Zbl 0788.68130 · doi:10.1007/BFb0037108
[12] Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1998) · Zbl 0906.18001
[13] Makkai, M.: First order logic with dependent sorts, FOLDS (1997) (Unpublished)
[14] Martin-Löf, P.: An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the Logic Colloquium 1973, pp. 73–118 (1975) · doi:10.1016/S0049-237X(08)71945-1
[15] Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007) · Zbl 05185799 · doi:10.1007/978-3-540-71209-1_40
[16] Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, Oxford (1990) · Zbl 0744.03029
[17] Oberschelp, A.: Untersuchungen zur mehrsortigen Quantorenlogik. Mathematische Annalen 145, 297–333 (1962) · Zbl 0101.25001 · doi:10.1007/BF01396685
[18] Paulson, L.: Isabelle: A Generic Theorem Prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994) · Zbl 0825.68059 · doi:10.1007/BFb0030541
[19] 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. 5, pp. 39–128. Oxford University Press, Oxford (2000)
[20] Rabe, F.: First-Order Logic with Dependent Types. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 377–391. Springer, Heidelberg (2006) · Zbl 1222.03016 · doi:10.1007/11814771_33
[21] Rabe, F.: Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen (2008)
[22] Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15, 91–110 (2002) · Zbl 1021.68082
[23] 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–28 (1985)
[24] Urban, J.: Translating Mizar for first-order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 203–215. Springer, Heidelberg (2003) · Zbl 1022.68622 · doi:10.1007/3-540-36469-2_16
[25] Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topić, 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. 1632, pp. 314–318. Springer, Heidelberg (1999)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.