Download PDFOpen PDF in browser

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

EasyChair Preprint 7719

10 pagesDate: April 4, 2022

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@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}}
Download PDFOpen PDF in browser