|  | 
|  | 
| | Vampire 2019: Keyword Index| Keyword | Papers | 
|---|
 | a |  | automated reasoning | Experimenting with Theory Instantiation in Vampire |  | automated theorem proving | Towards Word Sense Disambiguation by Reasoning Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
 |  | b |  | Bayesian optimisation | Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving |  | c |  | computer algebra | SAT, Computer Algebra, Multipliers |  | f |  | first-order theorem proving | Experimenting with Theory Instantiation in Vampire Aiming for the Goal with SInE
 |  | h |  | Heuristic Configuration | Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving |  | l |  | large theory problems | Aiming for the Goal with SInE |  | m |  | Multiplier circuits | SAT, Computer Algebra, Multipliers |  | n |  | Natural Language Processing | Towards Word Sense Disambiguation by Reasoning |  | o |  | Ontologies | Towards Word Sense Disambiguation by Reasoning |  | p |  | polynomial reasoning | SAT, Computer Algebra, Multipliers |  | premise selection | Aiming for the Goal with SInE Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
 |  | proof certificates | SAT, Computer Algebra, Multipliers |  | s |  | SAT | SAT, Computer Algebra, Multipliers |  | semantic mappings | Towards Word Sense Disambiguation by Reasoning |  | sine | Aiming for the Goal with SInE |  | SMT | Experimenting with Theory Instantiation in Vampire |  | SUMO | Towards Word Sense Disambiguation by Reasoning |  | Sumo Inference Engine (SInE) | Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving |  | t |  | theory instantiation | Experimenting with Theory Instantiation in Vampire |  | v |  | Vampire | Experimenting with Theory Instantiation in Vampire Aiming for the Goal with SInE
 | 
 | 
 | 
|