Linked Proofs Dataset
From Inference Web
Contents |
Overview
Linked Proofs is a Linking Open Data (LOD) dataset for thousands of formal proofs originally generated in TPTP project. The dataset is jointly published by the Tetherless World Constellation, Rensselaer Polytechnic Institute, and University of Miami. Linked proofs are highlighted by the following features:
- every formal proof is converted in to RDF/XML representation using Proof Markup Language (PML)
- individual proofs answering the same problem are interlinked by using obviously semantic equivalent formulae. Note, two formulae are obviously semantic equivalent if (i) their logic expression are syntactically equivalent after variable renaming and modulo permutation, and (ii) they are from the same context, e.g. answering the same TPTP problem.
Understanding the Dataset
Directory/File Organization
TPTP problems are grouped by domain. Each domain belongs to a main category and has one to many domain ids, each of which is labeled by a three letter string, e.g. PUZ. Each domain includes several TPTP problems. Each TPTP problem is associated with one to many TPTP solutions. For more information, see the Domain Structure of the TPTP Proofs. Here is an example:
Mathematics -- main category
Set theory -- domain
SEU -- the id of the domain
| http://inference-web.org/proofs/tptp/Problems/SEU/ | the directory that lists all SEU problems |
| http://inference-web.org/proofs/tptp/Problems/SEU/SEU140+2/ | the directory for a SEU problem |
| http://inference-web.org/proofs/tptp/Solutions/SEU/ | the directory that lists all solutions for all SEU problems |
| http://inference-web.org/proofs/tptp/Solution/SEU/SEU140+2/ | the directory for the solutions of a SEU problem |
| http://inference-web.org/proofs/tptp/Solutions/SEU/SEU140+2/EP---1.1/ | the directory for EP---1.1's solution of a SEU problem |
Solution file and related files
Given a TPTP solution, users should expected three files. The last two are shared by all solutions solving the same TPTP problem. Here is an example:
| answer (an RDF/XML file converted from EP---1.1's formal proof for a SEU problem) | http://inference-web.org/proofs/tptp/Solutions/SEU/SEU140+2/EP---1.1/answer.owl#answer | iwbrowser | source |
| query (an RDF/XML file for the formal description of the SEU problem) | http://inference-web.org/proofs/tptp/Problems/SEU/SEU140+2/query.owl | iwbrowser | source |
| question (an RDF/XML file for the English description of of the SEU problem) | http://inference-web.org/proofs/tptp/Problems/SEU/SEU140+2/questions.owl |
Accessing the Dataset
Browse
Resources
- TPTP website, http://tptp.org/
- Inference Web website, http://inference-web.org
Upcoming feature
- statistics about how axioms were reused by different proofs in each TPTP problem, here is a sample page http://inference-web.org/tmp/formulau/axiomu.html
Glossary
- leaf node: a ndoe without antecedents (aka. parents).
- leaf axioms: The leaf nodes of proofs of FOF problems are either from the original FOF problem, or have been introduced (soundly) by the ATP system. The analyis is wrt only the FOF leaf nodes that come from the original FOF problem.
