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
