CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Instantiation and pretending to be an SMT solver with VAMPIRE

G. Reger ; M. Suda ; Andrei Voronkov (Institutionen för Data- och informationsteknik, Formella metoder (Chalmers))
15th International Workshop on Satisfiability Modulo Theories, SMT 2017, Heidelberg, Germany, 22-23 July 2017 (1613-0073). Vol. 1889 (2017),
[Konferensbidrag, refereegranskat]

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).



Denna post skapades 2017-10-25.
CPL Pubid: 252763

 

Institutioner (Chalmers)

Institutionen för Data- och informationsteknik, Formella metoder (Chalmers)

Ämnesområden

Matematisk analys

Chalmers infrastruktur