∀x ∃y ∃z ((x ∨ z) ∧ y)
This particular formula is equivalent to true. (We can choose y and z to be true, then the formula evaluates to true both when x is true and when x is false.) In general, a QBF without free variables is equivalent either to true or to false.
A software tool that decides whether a given QBF is equivalent to true is called a QBF solver.
The goal of this project is to implement a QBF solver based on counter-example guided abstraction refinement (CEGAR) in the interactive proof assistant Isabelle, and to prove that its answers are correct. The CEGAR-based algorithm is described here.
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.