The TSTP Solution Library

A Library of Solutions

• Aim
  • A simple, unambiguous, source and reference mechanism
  • Set standards for ATP system output
  • Improve interpretation of ATP systems' output

• Motivation
  • System development by solution analysis
  • Solution processing by standard tools
  • System certification by solution verification

Features

• 80+ systems' TPTP derivations and models
• Resources beyond systems' PPPs
• Documented: System, Resources, SZS result and output, Statistics
• Human and computer readable: Name, Role, Logic, Source and user annotations
• A key - the TPTP language
  • Standards for writing derivations
  • Standards for writing finite and infinite Tarskian and Kripke interpretations

Browsing available online at tptp.org/TSTP