Top

Published in:

2018 | OriginalPaper | Chapter

Tactics and Certificates in Meta Dedukti

Author : Raphaël Cauderlier

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Tactics are often featured in proof assistants to simplify the interactive development of proofs by allowing domain-specific automation. Moreover, tactics are also helpful to check the output of automatic theorem provers because they can rebuild details that the provers omit.

We use meta-programming to define a tactic language for the Dedukti logical framework which can be used both for checking certificates produced by automatic provers and for developing proofs interactively.

More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped tactic language built on top of the typed one. We show the expressivity of these languages on two applications: a transfer tactic and a resolution certificate checker.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter The Coinductive Formulation of Common Knowledge

next chapter A Formalization of the LLL Basis Reduction Algorithm

By “untyped” we do not mean that no type is assigned to the Dedukti terms of the language but that typing is trivial: all the tactics have the same type (tactic).

Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, École Polytechnique (2015). https://tel.archives-ouvertes.fr/tel-01235303

Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, Berlin, Germany, 2–3 August 2015. Electronic Proceedings in Theoretical Computer Science, vol. 186, pp. 74–88. Open Publishing Association, Berlin, August 2015. https://doi.org/10.4204/EPTCS.186.8

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). http://smtlib.cs.uiowa.edu

Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24364-6_2CrossRef

Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414–420. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_29CrossRef

Blanco, R., Chihani, Z., Miller, D.: Translating between implicit and explicit versions of proof. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 255–273. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_16CrossRef

Boespflug, M., Carbonneaux, Q., Hermant, O.: The \(\lambda \varPi \)-calculus modulo as a universal proof language. In: David Pichardie, T.W. (ed.) The Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Manchester, vol. 878, pp. 28–43, June 2012. https://hal-mines-paristech.archives-ouvertes.fr/hal-00917845

Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552–593 (2013). https://doi.org/10.1017/S095679681300018XMathSciNetCrossRefMATH

Burel, G.: A shallow embedding of resolution and superposition proofs into the \(\lambda \varPi \)-calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, 9–10 June 2013. EPiC Series in Computing, vol. 14, pp. 43–57. EasyChair, Lake Placid, June 2013. http://www.easychair.org/publications/paper/141241

10.

Cauderlier, R., Dubois, C.: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 459–468. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_26CrossRef

11.

Cauderlier, R., Dubois, C.: FoCaLiZe and Dedukti to the rescue for proof interoperability. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 131–147. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_9CrossRef

12.

Cauderlier, R., Halmagrand, P.: Checking Zenon Modulo proofs in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings 4th Workshop on Proof eXchange for Theorem Proving, Berlin, Germany, 2–3 August 2015. Electronic Proceedings in Theoretical Computer Science, vol. 186, pp. 57–73. Open Publishing Association, Berlin, August 2015. https://doi.org/10.4204/EPTCS.186.7

13.

Cauderlier, R., Thiré, F.: Meta Dedukti. http://deducteam.gforge.inria.fr/metadedukti/

14.

Dorra, A.: Équivalence Curry-Howard entre le lambda-Pi-calcul et la logique intuitionniste (2010). Undergrad research intership report

15.

Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. PACMPL 1(ICFP), 34:1–34:29 (2017). https://doi.org/10.1145/3110278CrossRef

16.

Gilbert, F.: Proof certificates in PVS. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 262–268. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_17CrossRef

17.

Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_9CrossRefMATH

18.

Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Vito, B.D., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), pp. 56–68. No. NASA/CP-2003-212448 in NASA Technical Reports, September 2003. http://www.gilith.com/papers

19.

Kaiser, J.O., Ziliani, B., Krebbers, R., Régis-Gianas, Y., Dreyer, D.: Mtac2: Typed tactics for backward reasoning in Coq (2018, submitted for publication)

20.

McCune, W.: Prover9 and Mace4 (2005–2010). http://www.cs.unm.edu/~mccune/prover9/

21.

Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991). https://doi.org/10.1093/logcom/1.4.497MathSciNetCrossRefMATH

22.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965). https://doi.org/10.1145/321250.321253MathSciNetCrossRefMATH

23.

Saillard, R.: Type checking in the Lambda-Pi-Calculus Modulo: theory and practice. Ph.D. thesis, MINES Paritech (2015). https://pastel.archives-ouvertes.fr/tel-01299180

24.

Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009). https://doi.org/10.1007/s10817-009-9143-8MathSciNetCrossRefMATH

25.

Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015). https://doi.org/10.1017/S0956796815000118

26.

Zimmermann, T., Herbelin, H.: Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. CoRR abs/1505.05028 (2015). http://arxiv.org/abs/1505.05028

Title: Tactics and Certificates in Meta Dedukti
Author: Raphaël Cauderlier
Publisher: Springer International Publishing
Book: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner