Open AccessExperimenting with Theory Instantiation in Vampire
Author(s) -
Martin Riener
Publication year - 2020
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/pf85
Subject(s) - computer science , satisfiability modulo theories , vampire , avatar , modulo , programming language , theory , theoretical computer science , discrete mathematics , mathematics , human–computer interaction
Theory instantiation tackles the problem of theory reasoning with quantifiers in Vam- pire using an SMT solver. In contrast to AVATAR modulo theories it works locally by instantiating a clause such that its pure theory part becomes inconsistent and can be deleted. We report on the challenges when adding instantiation for the theory of arrays.