RAT elimination
From MaRDI portal
Cites work
- A theory of satisfiability-preserving proofs in SAT solving
- Clause elimination for SAT and QSAT
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient certified RAT verification
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Fast interpolating BMC
- First-order interpolation and interpolating proof systems
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Inprocessing rules
- Interpolant strength
- Interpolation and SAT-based model checking.
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Producing and verifying extremely large propositional refutations
- Resolution With Merging
- SAT-Based Model Checking without Unrolling
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- Towards a Semantics of Unsatisfiability Proofs with Inprocessing
- Verifying Refutations with Extended Resolution
This page was built for publication: RAT elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7024192)
