IW Meeting 2010-02-11

From Inference Web

Jump to: navigation, search


linked proof homepage

what data is available
the source of data
more details about the data http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml#The%20TPTP%20Domain%20Structure
how to use the data
some statistics about the data
example of the data

our workshop paper (proof quality)

  • everyone contribution, geoff will coordinate submission on position statement.

geoff-cynthia meeting notes

  • axiom formula usage: we've done
  • new equivalence computing module: cynthia got the code, we will use non-axiom usage to verify that via web interface (http://inference-web.org/tmp/formulau/NUM390+1/axiomUsed.html, we will reuse that on showing all non-axioms)
  • CNF formula usage: cynthia is working on it, we will have a bigger, we consider both leaf node (snark use CNF leaf node, but that is an intermediate node indeed, because they convert FOF to CNF, but didn't output that in TPTP).

linked proof paper improvement

  • we will defer the discussion to the next meeting when Deb is around.

publishing linked proofs

  <rdf:Description rdf:about="http://inference-web.org/proofs/linked/AGT/AGT001+1/mappings.owl#group3">
    <pmlr:hasMember rdf:resource="http://inference-web.org/proofs/linked/AGT/AGT001+1/EP---1.0pre/answer.owl#_-1961f636:1264195715e:-7f94"/>
    <pmlr:hasMember rdf:resource="http://inference-web.org/proofs/linked/AGT/AGT001+1/SInE---0.3/answer.owl#_-1961f636:1264195715e:-7eed"/>
    <pmlr:hasMember rdf:resource="http://inference-web.org/proofs/linked/AGT/AGT001+1/Ayane---1.1/answer.owl#_-1961f636:1264195715e:-7fed"/>
    <pmlr:hasMember rdf:resource="http://inference-web.org/proofs/linked/AGT/AGT001+1/VampireLT---10.0/answer.owl#_-1961f636:1264195715e:-7e55"/>
    <rdf:type rdf:resource="http://inference-web.org/2.0/pml-relation.owl#AllSame"/>
Personal tools