This webpage contains documents that I generated, like the Isabelle documentation from my PhD thesis. This is the only way to have links which survives changes in my affiliation.
SAT Solver Framework
As part of my PhD thesis, I developed a framework to formalize SAT solving. I still continue to expend it. It is not a very fast SAT solver, but you are guaranteed that the answer is correct and that there is no overflow happening internally that would compromise correctness.
Please refer to the IsaSAT page for more details.
I work with Armin Biere on SAT solving. One (rather obvious, but never written down before) result is that the standard minimization algorithm is complete in the sense that it remove all redundant literals (see more details in our SAT'21 paper). The result comes from a completeness theorem on Horn clauses.
Other interests include:
- parallel cube-and-conquer SAT solving with the SAT solver Paracooba.
- normal CDCL with our technique coined shrinking that reduces the size of learned clauses without increasing their glue. The technique is orthogonal to minimization. Shrinking shares the cache used for minimization.
One very useful tool of the interactive theorem prover Isabelle is the interaction with automatic theorem provers living outside. These tools come in two flavours:
- Sledgehammer: what facts do I need to prove this goal?
smt-tactic: let Isabelle check the proof you found for this goal!
I worked on integrated veriT into Sledgehammer during my master thesis, but I am now mostly focusing on the second approach. I have extended the tactic to include the SMT solver veriT and I am now working on integrating the SMT solver cvc5 – and unlike the work to integrate the Z3 in Isabelle by Böhme, the authors of cvc5 (especially Barbosa and Lachnitt) and veriT (especially Schurr) are helping me to make the proofs nicer and the reconstruction work easier!
In this direction, several people (including me) are attempting to define a proof format tentatively called Alethe that makes reconstruction easy enough.
External Links & Affilations
My current webpage can be found at http://fmv.jku.at/fleury/index.html. This page might or might not be more up-to-date than this one.
Before that I did my PhD at the MPI in Saarbrücken, Germany. My webpage there still exists, because I am still partially affiliated with the MPI.
My thesis comes with some fancy Isabelle documentation
available here and it would be too bad for the
links to get lost. The documentation refers to the
fleury-thesis branch of IsaFoL available at
I work in my free time on Isabelle-emacs available at https://github.com/m-fleury/isabelle-emacs/. It slightly extends Isabelle’s LSP server (no change is done to Isabelle’s kernel nor to Isabelle/jEdit) and make Isabelle usable for Emacs. If you don’t like Isabelle/jEdit or find it unstable and unusable, this provides an alternative.