Vampire getting noisy: Will random bits help conquer chaos? (system description)
From MaRDI portal
Publication:2104552
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
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Old or heavy? Decaying gracefully with age/weight shapes
- On SAT instance classes and a method for reliable performance experiments with SAT solvers
- Selecting the selection
- SETHEO: A high-performance theorem prover
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
Cited in
(7)- The 11th IJCAR automated theorem proving system competition – CASC-J11
- \texttt{gym-saturation}: gymnasium environments for saturation provers (system description)
- Efficient neural clause-selection reinforcement
- How much should this symbol weigh? A GNN-advised clause selection
- Regularization in Spider-style strategy discovery and schedule construction
- A higher-order Vampire (short paper)
- An empirical assessment of progress in automated theorem proving
Describes a project that uses
Uses Software
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)
