关于 SMT 理论设计：序列的情况
计算机科学中的逻辑
2024-11-05 v1
摘要
理论的语义与签名选择在决定该理论如何被使用以及推理该理论有多困难方面起着核心作用。本文关注序列的 SMT 理论。文献和当前最先进的 SMT 求解器中存在该理论的多种版本，但它尚未在 SMT-LIB 中标准化。我们反思其现有变体，并定义了一套理论设计准则，以帮助确定一个理论变体为何优于另一个。我们定义的准则也可用于评估其他理论的提案。基于这些准则，我们提出了一系列对序列 SMT 理论的修改建议，作为关于其标准化的讨论贡献。
引用
@article{arxiv.2411.01961,
title = {On SMT Theory Design: The Case of Sequences},
author = {Hichem Rami Ait El Hara and François Bobot and Guillaume Bury},
journal= {arXiv preprint arXiv:2411.01961},
year = {2024}
}