Vampire 2019: Keyword IndexKeyword  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  firstorder 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 

