×

Crystal: Integrating structured queries into a tactic language. (English) Zbl 1185.68618

Summary: We present the language \(\mathbf {CRStL}\) (\(\mathbf C\)ontrol \(\mathbf R\)ule \(\mathbf {St}\)rategy \(\mathbf L\)anguage, pronounce “crystal”) to formulate mathematical reasoning techniques as proof strategies in the context of the proof assistant \(\Omega \)mega. The language is arranged in two levels, a query language to access mathematical knowledge maintained in development graphs, and a strategy language to annotate the results of these queries with further control information. The two-leveled structure of the language allows the specification of proof techniques in a declarative way. We present the syntax and semantics of \(\mathbf {CRStL}\) and illustrate its use by examples.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N15 Theory of programming languages
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andersen, F., Petersen, K.D.: Recursive boolean functions in HOL. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991, pp. 367–377. IEEE Computer Society, Silver Spring (1992)
[2] Asperti, A., Padovani, L., Coen, C.S., Guidi, F., Schena, I.: Mathematical knowledge management in helm. Ann. Math. Artif. Intell. 38(1–3), 27–46 (2003) · Zbl 1025.68080 · doi:10.1023/A:1022907629104
[3] Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: Post-Proceedings of the Types 2004 International Conference. LNCS, vol. 3839, pp. 17–32. Springer, New York (2004) · Zbl 1172.68623
[4] Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. J. Autom. Reason. 39, 109–139 (2006) · Zbl 1132.68673 · doi:10.1007/s10817-007-9070-5
[5] Aspinall, D., Lüth, C., Wolff, B.: Assisted proof document authoring. In: Kohlhase, M. (ed.) Mathematical Knowledge Management MKM 2005, Lecture Notes in Artificial Intelligence, vol. 3863, pp. 65–80. Springer, New York (2006) · Zbl 1151.68658
[6] Autexier, S.: The CoRe calculus. In: Nieuwenhuis, R. (ed.) Proceedings of CADE-20, Tallinn, Estonia. LNAI, vol. 3632. Springer, New York (2005) · Zbl 1135.68549
[7] Autexier, S., Dietrich, D.: Synthesizing proof planning methods and Omega-Ants agents from mathematical knowledge. In: Borwein, J., Farmer, B. (eds.) Proceedings of MKM’06. LNAI, vol. 4108, pp. 94–109. Springer, New York (2006) · Zbl 1188.68277
[8] Autexier, S., Hutter, D.: Formal software development in maya. In: Hutter, D., Stephan, W. (eds.) Festschrift in Honor of J. Siekmann. LNAI, vol. 2605. Springer, New York (2006) · Zbl 1098.68549
[9] Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA. In: Kirchner, H., Ringeissen, Ce. (eds.) Proceedings 9th International Conference on Algebraic Methodology And Software Technology (AMAST’02). LNCS, vol. 2422. Springer, New York (2002) · Zbl 1057.68678
[10] Autexier, S., Benzmüller, C., Dietrich, D., Wagner, M.: Organisation, transformation, and propagation of mathematical knowledge in omega. J. Math. Comput. Sci. 2, 253–277 (2008) · Zbl 1176.68207 · doi:10.1007/s11786-008-0054-6
[11] Bancerek, G.: Information retrieval and rendering with mml query. In: Proceedings of MKM’06, pp. 266–279. Springer, New York (2006) · Zbl 1188.68125
[12] Bancerek, G., Rudnicki, P.: Information retrieval in mml. In: Proceedings of MKM’03, pp. 119–132. Springer, London (2003) · Zbl 1022.68610
[13] Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans.–Royal Soc., Math. Phys. Eng. Sci. 363(1835), 2351–2375 (2005) · Zbl 1152.03304 · doi:10.1098/rsta.2005.1650
[14] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development–Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, New York (2004) · Zbl 1069.68095
[15] Borovanský, P., Kirchner, H.: Strategies of elan: meta-interpretation and partial evaluation. In: Proceedings of International Workshop on Theory and Practice of Algebraic Specifications ASF+SDF 97, Workshops in Computing. Springer, Amsterdam (1997)
[16] Borovansky, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. Int. J. Found. Comput. Sci. 12(1), 69–95 (2001) · Zbl 1319.68125 · doi:10.1142/S0129054101000412
[17] Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk. R., Overbeek, R. (eds.) Proceedings CADE-9. LNAI, pp. 111–120. Springer, New York (1988) · Zbl 0656.68106
[18] Christian, J.: Flatterms, discrimination nets, and fast term rewriting. J. Autom. Reason. 10, 95–113 (1993) · doi:10.1007/BF00881866
[19] Constable, R.L., Allen, S.F., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D.J., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)
[20] Corbineau, P.: A declarative language for the coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES. Lecture Notes in Computer Science, vol. 4941, pp. 69–84. Springer, New York (2007) · Zbl 1138.68525
[21] Delahaye, D.: A proof dedicated meta-language. In: Proceedings of Logical Frameworks and Meta-Languages (LFM), Copenhagen (Denmark). ENTCS, vol. 70(2). Elsevier, Amsterdam (2002) · Zbl 1270.68262
[22] Dietrich, D.: The task-layer of the {\(\Omega\)}mega system. Diploma thesis, FR 6.2 Informatik, Universität des Saarlandes, Saarbrücken (2006)
[23] Dixon, L.: A proof planning framework for Isabelle. Ph.D. thesis, University of Edinburgh (2005)
[24] Dixon, L., Fleuriot, J.D.: A proof-centric approach to mathematical assistants. J. Appl. Logic 4(4), 505–532 (2005) · Zbl 1107.68096 · doi:10.1016/j.jal.2005.10.007
[25] Farmer, W., Guttman, J., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11, 653–654 (1993) · Zbl 0802.68129 · doi:10.1007/BF00881906
[26] Geuvers, H.: Proof assistants: history, ideas and future. Sadahana 34, 3–25 (2009) (Special Issue on Interactive Theorem Proving and Proof Checking) · Zbl 1192.68629 · doi:10.1007/s12046-009-0001-5
[27] Geuvers, H., Mamane, L.E.L.: A document-oriented Coq Plugin for Texmacs (2006)
[28] Gordon, M.: From lcf to hol: a short history. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 169–186. MIT, Cambridge (2000)
[29] Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF–a mechanised logic of computation. In: LNCS, vol. 78. Springer, New York (1979)
[30] Harrison, J.: Hol light: a tutorial introduction. In: Formal Methods in Computer-Aided Design (FMCAD’96), pp. 265–269. Springer, New York (1996)
[31] Huang, X.: Human oriented proof presentation: a reconstructive approach. In: DISKI, no. 112. Infix, Sankt Augustin (1996)
[32] Letichevsky, A.A.: Development of rewriting strategies. In: PLILP ’93: Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, pp. 378–390. Springer, London (1993) · Zbl 0794.68077
[33] Martí-Oliet, N., Meseguer, J., Verdejo, A.: Towards a strategy language for Maude. In: Martí-Oliet, N. (ed.) Proceedings Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, 27 March–4 April, 2004. Electronic Notes in Theoretical Computer Science, vol. 117, pp. 417–441. Elsevier, Amsterdam (2005)
[34] Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41–57 (2009). doi: 10.1016/j.jal.2007.07.004 · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[35] Mosses, P.D. (ed.): CASL reference manual. In: LNCS, no. 2960. Springer, New York (2004) · Zbl 1046.68001
[36] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL–a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer, New York (2002) · Zbl 0994.68131
[37] Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119–149 (1983) · Zbl 0551.68076 · doi:10.1016/0167-6423(83)90008-4
[38] Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Proc. FTP 97, pp. 119–124. Kluwer, Dordrecht (1998) · Zbl 0972.68520
[39] Richardson, J.: A semantics for proof plans with applications to interactive proof planning. In: Lecture Notes in Computer Science (2002) · Zbl 1023.68659
[40] Richardson, J., Smaill, A., Green, I.: System description: proof planning in higher-order logic with clam. In: 15th International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence, vol. 1421, pp. 129–133. Springer, New York (1998)
[41] Siekmann, J., Benzmüller, C., Autexier, S.: Computer supported mathematics with omega. J. Appl. Logic 4(4), 533–559 (2006) (Special issue on Mathematics Assistance Systems) · Zbl 1107.68101 · doi:10.1016/j.jal.2005.10.008
[42] Trybulec, A., Blair, H.: Computer assisted reasoning with Mizar. In: Joshi, A. (ed.) Proceedings of the 9th Int. Joint Conference on Artifical Intelligence. M. Kaufmann (1985) · Zbl 0568.68070
[43] Urban, J.: MoMM–fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. Artif. Intell. Tools 15(1), 109–130 (2006) · Zbl 05421611 · doi:10.1142/S0218213006002588
[44] Visser, E.: Stratego: a language for program transformation based on rewriting strategies. System description of Stratego 0.5. In: Middeldorp, A. (ed.) Rewriting Techniques and Applications (RTA 2001). Lecture Notes in Computer Science, vol. 2051, pp. 357–361. Springer, New York (2001) · Zbl 0981.68679
[45] Wallen, L.: Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. Series in Artificial Intelligence. MIT, Cambridge (1990) · Zbl 0782.03003
[46] Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., Topić, D.: SPASS version 2.0. In: Voronkov, A. (ed.) Automated Deduction–CADE-18. LNAI, no. 2392 , pp. 275–279. Springer, New York (2002) · Zbl 1072.68596
[47] Wenzel, M.: Isar–a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics: TPHOLs’99. LNCS, vol. 1690, pp. 167–184. Springer, New York (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.