Scalable Fine-Grained Proofs for Formula Processing
Scalable Fine-Grained Proofs for Formula Processing
复制标题
用于公式处理的可扩展细粒度证明
DOI：
10.1007/s10817-018-09502-y
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
P. Fontaine
中科院分区：
文献类型：
--
作者：
Haniel Barbosa;J. Blanchette;M. Fleury;P. Fontaine
我们提出了一个框架，用于处理自动定理证明器中的公式，生成详细的证明。主要组件是一个通用的上下文递归算法和一组可扩展的推理规则。封闭化，skolemization，理论特定的简化，和“让”表达式的扩展是这个框架的例子。使用合适的数据结构，证明生成只会增加线性时间开销，并且证明可以在线性时间内检查。我们在SMT求解器veriT中实现了该方法。这使我们能够大大简化代码库，同时增加了可以产生详细证明的问题的数量，这对于证明助手的独立检查和重建非常重要。为了验证该框架，我们在Isabelle/HOL中实现了证明重构。
We present a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of ‘let’ expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. To validate the framework, we implemented proof reconstruction in Isabelle/HOL.
来自机器生成的证明的半可理解的 Isar 证明
DOI：
10.1007/s10817-015-9335-3
发表时间：
2016
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Mathias Fleury;Steffen Juilf Smolka;Albert Steckermeier
通讯作者：
Albert Steckermeier
使用分析表和相关方法进行自动推理
DOI：
10.1007/978-3-642-40537-2_17
发表时间：
2013
期刊：
--
影响因子：
--
作者：
Khodadadi M
通讯作者：
Khodadadi M