TPTP-IW (Project)

From Inference Web

Jump to: navigation, search
Infobox (Project) edit with form
  • name: Linking Thousands of Problems for Theorem Provers and Inference Web
  • description: we investigate converting, linking, combining, improving proofs from TPTP library on the Inference Web.
  • relation(s): inference web
  • modified: 2011-7-11

Contents

People

Research

Knowledge Representation

  • convert Thousands of Problems for Theorem Provers (TPTP) to the Proof Markup Language (PML)and back
  • track versions of TPTP proofs
  • linking TPTP proofs into linked proofs
    • linking different versions of a proof
    • linking formulae by equivalent using owl:sameAs, computed using Geoff's tool
    • backtracking the provenance of combined proofs, it is related to explanation interface

Knowledge Discovery

  • combine and search for the optimal proof from the combined proofs and evaluate its complexity
  • rank proofs by deriving quantitative metrics for evaluating proof quality. Note - there may be multiple dimensions for use in evaluation, thus there may be no single best proof
  • compute and present the difference between two linked proofs
  • identify combinable proofs: now we have mizar - working on it, automate this process ?

Resources

Log

In Progress

  • Write up of some aspects
    • Motivating use cases (Paulo was going to generate a use case from UTEP science applications)
    • Geoff had a synthetic use case
  • Write up of Linked Proof foundation
Facts about TPTP-IW (Project)RDF feed
Dcterms:descriptionwe investigate converting, linking, combining, improving proofs from TPTP library on the Inference Web.
Dcterms:modified2011-7-11
Dcterms:relationInference web  +
Foaf:nameLinking Thousands of Problems for Theorem Provers and Inference Web
ParticipantDeborah L. McGuinness  +, Geoff Sutcliffe  +, Li Ding  +, Cynthia Chang  +, and Paulo Pinheiro da Silva  +
Skos:altLabelLinking Thousands of Problems for Theorem Provers and Inference Web  +
Personal tools
Navigation