Shortening QBF proofs with dependency schemes

DOI10.1007/978-3-319-66263-3_17zbMath1496.68364OpenAlexW2730075656WikidataQ59887551 ScholiaQ59887551MaRDI QIDQ1680258

Joshua Blinkhorn, Olaf Beyersdorff

Publication date: 15 November 2017

Full work available at URL: http://eprints.whiterose.ac.uk/118501/1/JLBdynamic.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Long-distance Q-resolution with dependency schemes ⋮ Unnamed Item ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF

Uses Software

• Chaff

This page was built for publication: Shortening QBF proofs with dependency schemes