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: Apr 28 2024 at 16:17 UTC