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

EasyChair Preprint no. 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 no. 7719},

  year = {EasyChair, 2022}}