Alethe: Towards a Generic SMT Proof Format (extended abstract)
Alethe: Towards a Generic SMT Proof Format (extended abstract)
复制标题
Alethe：迈向通用 SMT 证明格式（扩展摘要）
DOI：
10.4204/eptcs.336.6
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
P. Fontaine
中科院分区：
文献类型：
--
作者：
Hans;M. Fleury;Haniel Barbosa;P. Fontaine
The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format.
