QRAT^+: generalizing QRAT by a more powerful QBF redundancy property

DOI10.1007/978-3-319-94205-6_12MaRDI QIDQ1799077zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• QRATPre+: effective QBF preprocessing via strong redundancy properties
• On Stronger Calculi for QBFs
• QBFFam: a tool for generating QBF families from proof complexity
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• New resolution-based QBF calculi and their proof complexity
• Formal Methods in Computer-Aided Design
• On propositional QBF expansions and Q-resolution
• Beyond Q-resolution and prenex form: a proof system for quantified constraint satisfaction

Cited in

(9)

• How QBF expansion makes strategy extraction hard
• The equivalences of refutational QRAT
• QRAT polynomially simulates \(\forall\)-Exp+Res
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• Déjà Q All Over Again: Tighter and Broader Reductions of q-Type Assumptions
• Truth assignments as conditional autarkies
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Inconsistency proofs for ASP: the ASP-DRUPE format
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution

Describes a project that uses

Uses Software

• CAQE
• DepQBF
• DRAT-trim
• HQSpre

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799077)