Vampire 2019: Papers with Abstracts

Abstract. Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning. However parts of a multiplier, i.e., complex final stage adders are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. In this paper we focus on the implementation details of our new dedicated reduction engine, which not only allows fully automated adder substitution, but also employs polynomial re- duction efficiently. Our tool is furthermore able to generate proof certificates in the practical algebraic calculus and we also investigate the size of these proofs for one specific multiplier architecture.

Abstract. In this paper, we describe a practical application of Vampire for Word Sense Disam- biguation (WSD), which is an important research area in the field of Natural Language Processing (NLP). Its objective is choosing the intended sense of a word in a given context. In particular, we propose a method for the automatic disambiguation of the semantic rela- tions in BLESS, which is a dataset designed to evaluate models of distributional semantics, by choosing the WordNet synset it belongs to. For this purpose, we use the knowledge in Adimen-SUMO, which is obtained by means of a suitable transformation of the knowledge in the core of SUMO1 into first-order logic (FOL) and enables its use by FOL automated theorem provers such as Vampire. By exploiting the semantic mapping between WordNet and SUMO, we apply a black-box testing method that enables the automatic creation a set of conjectures for each word pair by considering the semantic relations provided by BLESS. Then, these conjectures are evaluated using Vampire and, according to the outcomes, each word is disambiguated to a single synset. Finally, we compare the results provided by our proposal and different disambiguation systems that can be found in the literature.

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

Abstract. The Sumo INference Engine (SInE) is a well-established premise selection algorithm for first-order theorem provers, routinely used, especially on large theory problems. The main idea of SInE is to start from the goal formula and to iteratively add other formulas to those already added that are related by sharing signature symbols. This implicitly defines a certain heuristical distance of the individual formulas and symbols from the goal.
In this paper, we show how this distance can be successfully used for other purposes than just premise selection. In particular, biasing clause selection to postpone introduction of input clauses further from the goal helps to solve more problems. Moreover, a precedence which respects such goal distance of symbols gives rise to a goal sensitive simplification ordering. We implemented both ideas in the automatic theorem prover Vampire and present their experimental evaluation on the TPTP benchmark.

Abstract. Modern theorem provers such as Vampire utilise premise selection algorithms to control the proof search explosion. Premise selection heuristics often employ an array of continuous and discrete parameters. The quality of recommended premises varies depending on the parameter assignment. In this work, we introduce a principled probabilistic framework for optimisation of a premise selection algorithm. We present results using Sumo Inference Engine (SInE) and the Archive of Formal Proofs (AFP) as a case study. Our approach can be used to optimise heuristics on large theories in minimum number of steps.