Linked Proofs Dataset

From Inference Web

Jump to: navigation, search

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

main category domain domain id(s) browse RDF/XML(problems) RDF/XML(solutions) TPTP(problems) TPTP(solutions)
Logic Combinatory logic COLBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Logic Logic calculi LCLBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Logic Henkin models HENBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Set theory SET
SEU
SEV
Browse
Browse
Browse
RDF/XML(Problems)
RDF/XML(Problems)
RDF/XML(Problems)
RDF/XML(Solutions)
RDF/XML(Solutions)
RDF/XML(Solutions)
TPTP(Problems)
TPTP(Problems)
TPTP(Problems)
TPTP(Solutions)
TPTP(Solutions)
TPTP(Solutions)
Mathematics Graph theory GRABrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Relation algebra RELBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Boolean algebra BOOBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Robbins algebra ROBBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Left distributive LDABrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Lattices LATBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Quantales QUABrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Kleene algebra KLEBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Groups GRPBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Rings RNGBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Fields FLDBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) Homological algebra HALBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics (algebra) General algebra ALGBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Number theory NUMBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Topology TOPBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Analysis ANABrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Geometry GEOBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Mathematics Category theory CATBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Computing theory COMBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Knowledge representation KRSBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Natural Language Processing NLPBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Planning PLABrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Agents AGTBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Commonsense Reasoning CSRBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Software creation SWCBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Computer science Software verification SWVBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Science and Engineering Hardware creation HWCBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Science and Engineering Hardware verification HWVBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Science and Engineering Medicine MEDBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Science and Engineering Processes PROBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Social sciences Management MGTBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Social sciences Geography GEGBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Other Syntactic SYN
SYO
Browse
Browse
RDF/XML(Problems)
RDF/XML(Problems)
RDF/XML(Solutions)
RDF/XML(Solutions)
TPTP(Problems)
TPTP(Problems)
TPTP(Solutions)
TPTP(Solutions)
Other Puzzles PUZBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)
Other Miscellaneous MSCBrowseRDF/XML(Problems) RDF/XML(Solutions) TPTP(Problems) TPTP(Solutions)

Resources

Upcoming feature

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.
Personal tools
Navigation