AltGr-Ergo，SMT求解器Alt-Ergo的图形用户界面
AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo
摘要：
由于一阶逻辑的不可判定性和复杂性，SMT求解器可能不会终止于某些问题或需要很长的时间。当这种情况发生时，人们希望找到求解器失败的原因。为此，我们设计了AltGr-Ergo，这是SMT求解器Alt-Ergo的交互式图形界面，允许用户和工具开发人员帮助求解器完成一些证明。AltGr-Ergo提供实时的反馈，以评估和量化求解器的进度，并提供各种语法操作选项，以允许与Alt-Ergo进行更细粒度的交互。本文描述了这些功能及其实现，并给出了其中大多数功能的使用场景。
英文摘要：
Due to undecidability and complexity of first-order logic, SMT solvers may not terminate on some problems or require a very long time. When this happens, one would like to find the reasons why the solver fails. To this end, we have designed AltGr-Ergo, an interactive graphical interface for the SMT solver Alt-Ergo which allows users and tool developers to help the solver finish some proofs. AltGr-Ergo gives real time feedback in order to evaluate and quantify progress made by the solver, and also offers various syntactic manipulation options to allow a finer grained interaction with Alt-Ergo. This paper describes these features and their implementation, and gives usage scenarios for most of them.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
