Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):
G. Reger, M. Suda, A. Voronkov:
"Instantiation and Pretending to be an SMT Solver with Vampire";
Vortrag: SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories,
Heidelberg, Germany;
22.07.2017
- 23.07.2017.
Kurzfassung englisch:
This paper aims to do two things. Firstly, it discusses how the VAMPIRE automatic theorem prover
both succeeds and fails at pretending to be an SMT solver. We discuss how Vampire reasons with
problems containing both quantification and theories, the limitations this places on what it can do, and
the advantages this provides over the standard SMT approach. Secondly, it focuses on the problem of
instantiation of quantified formulas and asks whether VAMPIRE needs it (it does) and whether it can
directly borrow techniques from SMT solving (maybe).
Schlagworte:
automated theorem proving, theory reasoning, SMT
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264625.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.