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

DOI10.1007/978-3-031-10769-6_38MaRDI QIDQ2104552zbMATH OpenOpenAlexFDO

Authors Martin Suda

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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

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

Cited in

(2)

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

Describes a project that uses

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)