AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo

Sylvain Conchon
(LRI, Université Paris-Sud)
Mohamed Iguernlala
(OCamlPro SAS)
Alain Mebsout
(The University of Iowa)

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.

In Serge Autexier and Pedro Quaresma: Proceedings of the 12th Workshop on User Interfaces for Theorem Provers (UITP 2016), Coimbra, Portugal, 2nd July 2016, Electronic Proceedings in Theoretical Computer Science 239, pp. 1–13.
Published: 24th January 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.239.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org