IW Meeting 2009-02-26

From Inference Web

Jump to: navigation, search



review IW Meeting 2009-02-19

backtrack provenance of combined proof

mizar translation I have generated PML proofs for Mizar xboole_1 and newton as Geoff suggested, almost. All xboole_1 proofs were generated smoothly, but a bounch of newton proofs failed. The failed newton proofs are t5, t11,t30-t32, t35, t36, t38-t41, t43, t45,t47,t50,t51,t78,t79, t81,t86,t96-t99 and t101. From what I can see, they all have larger size than most of the others. I am wondering if they are also different structurally. Here is the url leads to the Mizar proofs: http://inference-web.org/proofs/tptp/MizarProofs/

Another thing is that I also used the program Geoff sent to generate pml query(problem) strings. The query strings I have checked are long. For example, take a look of: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FMizarProofs%2Fxboole_1%2Fxboole_1__t1_xboole_1.owl%23answer

In a previous meeting I said I would generate a report for each combined proof. I've just got the first cut of it. Please take a look of an example: http://inference-web.org/proofs/tptp/Solutions/SWC/SWC028+1/Metis---2.1/combined30.tptp.report.html

honglei graph diff

combine proof report

PML on Wiki http://tw2.tw.rpi.edu/wiki/r2d2/index.php/Mizar_Test1

dump term equivalence relation


backtrack provenance of combined proof

  • is_explanation_of in pmlj
    • rename to has original proof
    • remove max cardinality
    • make it a fully ordered list

equivalence relation


  • todo - cynthia will generate an example and go over with paulo BEFORE the next meeting.
Facts about IW Meeting 2009-02-26RDF feed
Date26 February 2009  +
Personal tools