论文标题
依赖类型理论的自动推理的组成预处理
Compositional pre-processing for automated reasoning in dependent type theory
论文作者
论文摘要
在基于相关类型理论的交互式定理掠夺的背景下，自动化策略（专用决策程序，自动求解器的呼吁，...）通常仅限于完全存在于某些预期的逻辑片段中的目标。这通常会阻止用户在其他情况下（甚至类似的情况）应用这些策略。 本文讨论了在COQ证明助手中自动化正式证明的预处理操作的设计和实施。它提出了实施各种可预测的原子目标变换，可以通过各种方式组成，以针对不同的后端。一个示例画廊说明了它如何有助于显着扩大自动化引擎的功能。
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.
