Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
G. Reger, N. Bjorner, M. Suda, A. Voronkov:
"AVATAR Modulo Theories";
Vortrag: GCAI 2016 / 2nd Global Conference on Artificial Intelligence,
Berlin, Germany;
29.09.2016
- 02.10.2016; in: "GCAI 2016. 2nd Global Conference on Artificial Intelligence",
EasyChair,
EPiC Series in Computing / 41 / Berlin
(2016),
S. 39
- 52.
Kurzfassung englisch:
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.
Schlagworte:
Theorem Proving, Satisfiability Modulo Theories, First Order Logic, Automated Reasoning, Vampire, Z3
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_255030.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.