AltGr-Ergo：SMT求解器Alt-Ergo的图形用户界面
人机交互
2017-01-31 v1 计算机科学中的逻辑
摘要
由于一阶逻辑的不确定性和复杂性，SMT 求解器可能在某些问题上不终止或需要很长时间。当这种情况发生时，人们希望找到求解器失败的原因。为此，我们设计了 AltGr-Ergo，一个用于 SMT 求解器 Alt-Ergo 的交互式图形用户界面，它允许用户和工具开发者帮助求解器完成一些证明。AltGr-Ergo 提供实时反馈以评估和量化求解器取得的进展，并且还提供各种语法操作选项以允许与 Alt-Ergo 更细粒度的交互。本文描述了这些特性及其实现，并给出了大多数特性的使用场景。
引用
@article{arxiv.1701.07124,
title = {AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo},
author = {Sylvain Conchon and Mohamed Iguernlala and Alain Mebsout},
journal= {arXiv preprint arXiv:1701.07124},
year = {2017}
}
备注
In Proceedings UITP 2016, arXiv:1701.06745