Talks and Poster Presentations (with Proceedings-Entry):
G. Reger, N. Bjorner, M. Suda, A. Voronkov:
"AVATAR Modulo Theories";
Talk: GCAI 2016 / 2nd Global Conference on Artificial Intelligence,
- 2016-10-02; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence",
EPiC Series in Computing / 41 / Berlin
This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.
Theorem Proving, Satisfiability Modulo Theories, First Order Logic, Automated Reasoning, Vampire, Z3
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.