Vampire getting noisy: Will random bits help conquer chaos? (system description)
type: Item
instance of: scholarly article
title: Vampire getting noisy: Will random bits help conquer chaos? (system description)
DOI: 10.1007/978-3-031-10769-6_38
author: Martin Suda
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628214
zbMATH Keywords: saturation-based proving
zbMATH Keywords: evalutation
zbMATH Keywords: randomization
describes a project that uses: ileanCoP
describes a project that uses: BanditFuzz
describes a project that uses: SETHEO
describes a project that uses: TPTP
describes a project that uses: leanCoP
describes a project that uses: AVATAR
describes a project that uses: randoCoP
describes a project that uses: VAMPIRE
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 38
OpenAlex ID: W4289104037
cites work: On SAT instance classes and a method for reliable performance experiments with SAT solvers
cites work: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
cites work: Selecting the Selection
cites work: Clause Elimination Procedures for CNF Formulas
cites work: Blocked Clauses in First-Order Logic
cites work: SETHEO: A high-performance theorem prover
cites work: leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
cites work: Old or heavy? Decaying gracefully with age/weight shapes
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: AVATAR: The Architecture for First-Order Theorem Provers
description: scientific article; zbMATH DE number 7628214