Re: [Hol-developers] which defCNF?

[Joe H. <jo...@gi...>]

There's another one in the metis directory, too. The answer probably
depends on your application - what are you trying to use it for? Is it
just propositional, quantified boolean or first order?

Joe

On Mon, Apr 21, 2008 at 2:50 PM, Konrad Slind <sl...@cs...> wrote:
> Hi all,
>
>   Which translation to CNF should one use? Seems like there are at
>  least 3:
>
>    src/Canon.CNF_CONV
>    src/HolSat.def_cnf       (does not return a theorem, but that's OK)
>    examples/HolCheck/defCNF.DEF_CNF_VECTOR_CONV
>
>  Thanks,
>  Konrad.
>
>  -------------------------------------------------------------------------
>  This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
>  Don't miss this year's exciting event. There's still time to save $100.
>  Use priority code J8TL2D2.
>  http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
>  _______________________________________________
>  Hol-developers mailing list
>  Hol...@li...
>  https://lists.sourceforge.net/lists/listinfo/hol-developers
>