Friday 11 March 2016, 10:30: Archsat: SMT, Tableaux and beyond, Guillaume Bury (Inria).

Archsat is a prototype theorem prover which uses a SAT solver as its core, but also integrates methods from first order theorem prover in order to find instantiations. It is designed to experiment with various techniques in theorem proving.

The ground part of the reasoning done in Archsat is done using an extension of the usual SMT architecture called McSat, which stand for Model Constructing Sat. It consists of deciding not only on the truth value of atomic propositions, but also on the model assignment of terms occuring in the problem, so that at the end, the solver can return a full model of the input formulas (compared to a propositional model only for typical SMT solvers).

Reasoning about quantified formulas is currently done through the use of meta-variables, much like what is done in the Tableaux theorem prover Zenon. There are currently two mechanisms for instantiation, one similar to Zenon's, and another which uses constraints to incrementally close branches during the proof search.