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 , vampire , satisfiability modulo theories , 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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom