\({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property

DOI10.1007/978-3-319-94205-6_12OpenAlexW3103481621MaRDI QIDQ1799077

Florian Lonsing, Uwe Egly

Publication date: 18 October 2018

Full work available at URL: https://arxiv.org/abs/1804.02908

Mathematics Subject Classification ID

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

Related Items (5)

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Truth Assignments as Conditional Autarkies ⋮ How QBF expansion makes strategy extraction hard ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers

Uses Software

• DepQBF
• DRAT-trim
• CAQE
• HQSpre

This page was built for publication: \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property