Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Verified QBF Solving

Email Gateway (Mar 08 2024 at 09:01):

From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I’m happy to announce a new AFP entry by Axel Bergström and Tjark Weber

Verified QBF Solving

A Quantified Boolean Formula (QBF) extends propositional logic with
quantification over Boolean variables. We formalise two simple QBF solvers and
prove their correctness. One solver is based on naive quantifier expansion,
while the other utilises a search-based algorithm. Additionally, we formalise a
parser for the QDIMACS input format and use Isabelle's code generation feature
to obtain executable versions of both solvers.

https://www.isa-afp.org/entries/QBF_Solver_Verification.html

Enjoy,
René

Last updated: Jan 04 2025 at 20:18 UTC