Hi John,
you can get a very detailed and easily checkable output from Prover9 by
using its Ivy proof objects (they are so simple that I even wrote a Mizar
import for it :-). It used to be an option to Otter, but it seems that
Bill now has a special tool for it: prooftrans
http://www.cs.unm.edu/~mccune/prover9/manual/2008-04A/prooftrans.html .
Search for IVY Proofs on that page.
Josef
On Wed, 16 Apr 2008, John Harrison wrote:
>
> Hi Tom,
>
> | I have a problem running the following example:
> | [...]
>
> Thanks for reporting that! It turns out that I was only doing proof
> reconstruction for paramodulation with unit equations, not general
> clauses. I've put in a fix that I think corrects things generally, and
> certainly solves the problem you wanted. But let me know if you hit
> other failures. Prover9 is distinguished from most other systems by
> the fact that it provides very clear and explicit low-level proofs.
> But the proof format is not really documented, and I essentially
> reverse-engineered it from a few examples, so other flaws are
> possible. My proposed fix is to add the following extra functions:
>
> let AP_IMP =
> let pp = MATCH_MP(TAUT `(a ==> b) ==> !x. x \/ a ==> x \/ b`) in
> fun t -> SPEC t o pp;;
>
> let rec PARA_BACK_CONV eqdir tm =
> match eqdir with
> [Atom "1"] when not(is_disj tm) -> REFL tm
> | [Atom "2"] when not(is_disj tm) -> SYM_CONV tm
> | Atom "2"::eqs -> RAND_CONV (PARA_BACK_CONV eqs) tm
> | [Atom "1"; Atom f] when is_disj tm ->
> let th1 = if f = "2" then LAND_CONV SYM_CONV tm else REFL tm in
> let tm' = rand(concl th1) in
> let djs = disjuncts tm' in
> let th2 = DISJ_ACI_RULE(mk_eq(tm',list_mk_disj(tl djs @ [hd djs])))
> in
> TRANS th1 th2
> | _ -> failwith "PARA_BACK_CONV";;
>
> and then change the "paramod" clause in the definition of "proofstep" from
>
> | List[Atom "paramod"; Atom eqid; List [Atom flip]; Atom tmid; List dir] ->
> let eth = (if flip = "2" then SYM else I) (apply asms eqid)
> and tth = apply asms tmid
> and path = (map (fun (Atom s) -> int_of_string s) dir) in
> let th = CONV_RULE(PARA_SUBS_CONV path eth) tth in
> if concl th = tm then th
> else failwith "Inconsistency from instantiation"
>
> to:
>
> | List[Atom "paramod"; Atom eqid; List eqdir; Atom tmid; List dir] ->
> let eth = CONV_RULE (PARA_BACK_CONV eqdir) (apply asms eqid)
> and tth = apply asms tmid
> and path = (map (fun (Atom s) -> int_of_string s) dir) in
> let etm = concl eth in
> let th =
> if is_disj etm then
> let djs = disjuncts etm in
> let eq = last djs in
> let fth = CONV_RULE (PARA_SUBS_CONV path (ASSUME eq)) tth in
> MP (itlist AP_IMP (butlast djs) (DISCH eq fth)) eth
> else CONV_RULE(PARA_SUBS_CONV path eth) tth in
> if concl th = tm then th
> else failwith "Inconsistency from paramodulation"
>
> | Related to this example, I have a question about the standard options in
> | file prover9.ml:
> |
> | let prover9_options = ref
> | ("clear(auto_inference).\n"^
> | "clear(auto_denials).\n"^
> | "clear(auto_limits).\n"^
> | "set(neg_binary_resolution).\n"^
> | "set(binary_resolution).\n"^
> | "set(paramodulation).\n");;
> |
> | If I run with these options prover9 takes a long time, but if I run
> | with the default prover9 settings (by modifying the prover9.ml
> | file), prover9 proves the goal very quickly. However, I suspect
> | that it may only be proving a single disjunct rather than all the
> | disjuncts (?). Can you confirm this?
>
> No, based on the fact that (with that bugfix) the proof reconstruction
> for your example still works when I set
>
> prover9_options := ""
>
> (this is what you meant by using the default settings, right?), it
> must be doing the whole thing. But I also found that the default
> settings were much faster in this case. The settings in the file
> were arrived at based on a bit of empirical investigation on some
> examples, and might not be the best choice in general. I can't even
> remember what objection I had to the default options.
>
> John.
>
> -------------------------------------------------------------------------
> 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-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
-------------------------------------------------------------------------
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-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
