Validating QBF Invalidity in HOL4

DOI10.1007/978-3-642-14052-5_32zbMath1291.68375OpenAlexW1935328433MaRDI QIDQ5747670

Tjark Weber

Publication date: 14 September 2010

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_32

Mathematics Subject Classification ID

Related Items (2)

Validating QBF Validity in HOL4 ⋮ Proving Valid Quantified Boolean Formulas in HOL Light

Uses Software

• Coq
• Isabelle
• PVS
• HOL
• Squolem

This page was built for publication: Validating QBF Invalidity in HOL4