扩展 SMTCoq：一个经过认证的 SMT 检查器（扩展摘要）
计算机科学中的逻辑
2016-06-21 v1
摘要
本扩展摘要报告了 SMTCoq 的当前进展，SMTCoq 是 Coq 证明助手与外部 SAT 和 SMT 求解器之间的通信工具。基于在 Coq 中实现并证明正确的通用一阶证书检查器，SMTCoq 提供了既能检查外部 SAT 和 SMT 答案，又能以安全方式利用此类求解器改进 Coq 自动化的功能。SMTCoq 目前支持 SAT 求解器 zChaff，以及支持同余闭包与线性整数算术理论组合的 SMT 求解器 veriT，其设计旨在以合理的工作量进行扩展：我们介绍了支持 SMT 求解器 CVC4 和位向量理论的进行中工作。
引用
@article{arxiv.1606.05947,
title = {Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)},
author = {Burak Ekici and Guy Katz and Chantal Keller and Alain Mebsout and Andrew J. Reynolds and Cesare Tinelli},
journal= {arXiv preprint arXiv:1606.05947},
year = {2016}
}
备注
In Proceedings HaTT 2016, arXiv:1606.05427