Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)

EasyChair Preprint 7719

Abstract

Treating a saturation-based automatic theorem prover (ATP) as a Las Vegas randomized algorithm is a way to illuminate the chaotic nature of proof search and make it amenable to study by probabilistic tools. On a series of experiments with the ATP Vampire, the paper showcases some implications of this perspective for prover evaluation.

Keyphrases: evaluation, randomization, saturation-based theorem proving

@booklet{EasyChair:7719,
  author    = {Martin Suda},
  title     = {Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)},
  howpublished = {EasyChair Preprint 7719},
  year      = {EasyChair, 2022}}