# TPTP-IW (Project)

### From Inference Web

| ||

## 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

- TPTP project
- Linked Proofs Dataset - a dataset we used for our research
- Combine and Improve TPTP Proofs - a demo on how TPTP proofs can be improved.

## Log

- (July 21,2008) The TPTP-PML tools demo is released. http://www.cs.miami.edu/~geoff/Guest/

## 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:description | we investigate converting, linking, combining, improving proofs from TPTP library on the Inference Web. |

Dcterms:modified | 2011-7-11 |

Dcterms:relation | Inference web + |

Foaf:name | Linking Thousands of Problems for Theorem Provers and Inference Web |

Participant | Deborah L. McGuinness +, Geoff Sutcliffe +, Li Ding +, Cynthia Chang +, and Paulo Pinheiro da Silva + |

Skos:altLabel | Linking Thousands of Problems for Theorem Provers and Inference Web + |