Email Gateway (Aug 18 2022 at 14:24): Email Gateway (Aug 18 2022 at 14:24):From: Gerwin Klein <gerwin.klein@nicta.com.au>
The Archive of Formal Proofs is now updated to the latest Isabelle release. All entries from the main page work with Isabelle2009-1, old versions remain accessible from the individual entry pages.
With the update come two new entries:
A Fast SAT Solver for Isabelle in Standard ML
by Armin Heller
http://afp.sourceforge.net/entries/DPT-SAT-Solver.shtml
This contribution contains a fast SAT solver for Isabelle written in Standard ML. By loading the theory DPT_SAT_Solver, the SAT solver installs itself (under the name ``dptsat'') and certain Isabelle tools like Refute will start using it automatically. This is a port of the DPT (Decision Procedure Toolkit) SAT Solver written in OCaml.
and
Formalizing the Logic-Automaton Connection
by Stefan Berghofer and Markus Reiter
http://afp.sourceforge.net/entries/Presburger-Automata.shtml
This work presents a formalization of a library for automata on bit strings. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle's code generator. With this work, we therefore provide a mechanized proof of a well-known connection between logic and automata theory. The formalization is also described in a publication [TPHOLs 2009].
Cheers,
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC