Re: [isabelle-dev] isabelle dimacs2hol
On Thu, 2013-08-01 at 16:41 +0200, Makarius wrote: On Wed, 10 Jul 2013, Tjark Weber wrote: Looking superficially at http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy I wonder if this actually works right now. Good question. One issue is that the theory requires a SAT solver (zChaff or MiniSat) to work properly. These days, one could probably be shipped as a component, but I wonder if that's worth it. People just don't seem to use Isabelle to prove large propositional tautologies. I still think that encodings of decidable problems into propositional logic could probably be just as beneficial in theorem proving as they've been in many other domains. But regarding the future of sat, I am rather undecided at this point. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle dimacs2hol
On Wed, 10 Jul 2013, Tjark Weber wrote: I vaguely remember a private discussion about the performance of inner syntax parsing in this respect. For a realistic import one would bypass that anyway, i.e. not generate source files to parse them again, but read things directly via some Isabelle/ML functions. Agreed. Related functionality is available in HOL/ex/SAT_Examples.thy. (Cleaning up old mail threads ...) Looking superficially at http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy I wonder if this actually works right now. It used to be subject to try use_thy ... for several years, and the current HOL/ROOT has it commented-out. If you have some ambition to put it into shape, I can give some hints what needs to be done. E.g. global ML reference variables need to be eliminated and replaced by configuration options in ML (structure Config with certain operations in structure Attrib) or system options in ML/Scala (which are subject to persistent user preferences, potentially available in the front-end). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle dimacs2hol
On Tue, 9 Jul 2013, Tjark Weber wrote: On Mon, 2013-07-08 at 11:09 +0200, Makarius wrote: Does the Isabelle tool dimacs2hol from 2004 still have a purpose? The DIMACS CNF format appears to be an old proposal for SAT, predating newer things like SMT-LIB. So this looks like a candidate for deletion. DIMACS CNF remains the standard input format for SAT solvers. Describing it as outdated wouldn't do justice to the SAT research community. You have a link there from 2004, pointing to a paper from 1993, which seems to predate what they call the official DIMACS CNF format. (On Mac OS X I even failed to open that DVI file on the spot.) So at first sight it looks unmaintained, and the usual reaction is either to brush it up, or keep the history in the history (via hg rm). I used the tool in order to benchmark the Isabelle/HOL integration of SAT solvers. This requires a full round trip, i.e., not just export of propositional Isabelle/HOL formulae into DIMACS CNF, but also import of DIMACS CNF benchmarks into Isabelle/HOL. I vaguely remember a private discussion about the performance of inner syntax parsing in this respect. For a realistic import one would bypass that anyway, i.e. not generate source files to parse them again, but read things directly via some Isabelle/ML functions. Incidently, this recent thread on isabelle-users https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-May/msg00118.html shows that the inner syntax parser is not the only bottle-neck, due to so many add-on layers in the term-check phase (and repeated term certify). Anyway, shall I do the hg rm of the two relevant files now? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
