Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2204.02643 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911780707500032 |
|---|---|
| author | Blot, Valentin Cousineau, Denis Crance, Enzo de Prisque, Louise Dubois Keller, Chantal Mahboubi, Assia Vial, Pierre |
| author_facet | Blot, Valentin Cousineau, Denis Crance, Enzo de Prisque, Louise Dubois Keller, Chantal Mahboubi, Assia Vial, Pierre |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2204_02643 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Compositional pre-processing for automated reasoning in dependent type theory Blot, Valentin Cousineau, Denis Crance, Enzo de Prisque, Louise Dubois Keller, Chantal Mahboubi, Assia Vial, Pierre Logic in Computer Science 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. |
| title | Compositional pre-processing for automated reasoning in dependent type theory |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2204.02643 |