Alethe：迈向一种通用 SMT 证明格式（扩展摘要）
计算机科学中的逻辑
2021-07-07 v1
摘要
SMT 求解器 veriT 所用证明格式的第一版于十年前在首届 PxTP 研讨会上提出。自那时起，该格式已趋于成熟。veriT 证明被用于多种应用中，且其他求解器也以相同格式生成证明。我们现在希望从社区收集反馈以指导未来的发展。为此，我们回顾该格式的历史，介绍我们开发该格式的务实方法，并讨论其他求解器使用该格式时可能出现的问题。
引用
@article{arxiv.2107.02354,
title = {Alethe: Towards a Generic SMT Proof Format (extended abstract)},
author = {Hans-Jörg Schurr and Mathias Fleury and Haniel Barbosa and Pascal Fontaine},
journal= {arXiv preprint arXiv:2107.02354},
year = {2021}
}
备注
In Proceedings PxTP 2021, arXiv:2107.01544