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

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

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)

Related Items

The 11th IJCAR automated theorem proving system competition – CASC-J11

Uses Software

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

Cites Work

• SETHEO: A high-performance theorem prover
• 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
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• Old or heavy? Decaying gracefully with age/weight shapes
• Selecting the Selection
• AVATAR: The Architecture for First-Order Theorem Provers
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• Blocked Clauses in First-Order Logic
• Clause Elimination Procedures for CNF Formulas