Compositional pre-processing for automated reasoning in dependent type theory
In: CPP 2023 - Certified Programs and Proofs ; https://inria.hal.science/hal-03901019 ; CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩, 2023
Online
Konferenz
Zugriff:
International audience ; In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, .) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.
| Titel: |
Compositional pre-processing for automated reasoning in dependent type theory
|
|---|---|
| Autor/in / Beteiligte Person: | Blot, Valentin ; Cousineau, Denis ; Crance, Enzo ; Dubois de Prisque, Louise ; Keller, Chantal ; Mahboubi, Assia ; Vial, Pierre ; Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Mitsubishi Electric R&D Centre Europe France (MERCE-France) ; Mitsubishi Electric France ; Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE) ; Inria Rennes – Bretagne Atlantique ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-École Centrale de Nantes (Nantes Univ - ECN) ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes université - UFR des Sciences et des Techniques (Nantes univ - UFR ST) ; Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Nantes Université (Nantes Univ)-Nantes Université - pôle Sciences et technologie ; Nantes Université (Nantes Univ)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique) ; Nantes Université (Nantes Univ) ; Laboratoire des Sciences du Numérique de Nantes (LS2N) ; Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA) ; Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) |
| Link: | |
| Zeitschrift: | CPP 2023 - Certified Programs and Proofs ; https://inria.hal.science/hal-03901019 ; CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩, 2023 |
| Veröffentlichung: | HAL CCSD, 2023 |
| Medientyp: | Konferenz |
| DOI: | 10.1145/3573105.3575676 |
| Schlagwort: |
|
| Sonstiges: |
|