Vampire getting noisy: Will random bits help conquer chaos? (system description)

DOI10.1007/978-3-031-10769-6_38OpenAlexW4289104037MaRDI QIDQ2104552FDOQ2104552

Martin Suda

Publication date: 7 December 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_38

zbMATH Keywords

randomizationevalutationsaturation-based proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• SETHEO: A high-performance theorem prover
• AVATAR: The Architecture for First-Order Theorem Provers
• Clause Elimination Procedures for CNF Formulas
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• On SAT instance classes and a method for reliable performance experiments with SAT solvers
• Selecting the Selection
• Old or heavy? Decaying gracefully with age/weight shapes
• Blocked Clauses in First-Order Logic

Cited In (2)

• The 11th IJCAR automated theorem proving system competition – CASC-J11
• \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)

Uses Software

• SETHEO
• VAMPIRE
• TPTP
• leanCoP
• ileanCoP
• randoCoP
• AVATAR
• BanditFuzz

This page was built for publication: Vampire getting noisy: Will random bits help conquer chaos? (system description)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104552)