Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Scopus citations


This paper gives an overview of activities and products that stem from the Thousands of Problems for Theorem Provers (TPTP) problem library for Automated Theorem Proving (ATP) systems. These include the TPTP itself, the Thousands of Solutions from Theorem Provers (TSTP) solution library, the CADE ATP System Competition (CASC), tools such as my semantic Derivation Verifier (GDV) and the Interactive Derivation Viewer (IDV), meta-ATP systems such as the Smart Selective Competition Parallelism (SSCPA) system and the Semantic Relevance Axiom Selection System (SRASS), and applications in various domains.

Original languageEnglish (US)
Title of host publicationComputer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783540745099
StatePublished - Jan 1 2007
Event2nd International Symposium on Computer Science in Russia, CSR 2007 - Ekaterinburg, Russian Federation
Duration: Sep 3 2007Sep 7 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4649 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other2nd International Symposium on Computer Science in Russia, CSR 2007
CountryRussian Federation

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'TPTP, TSTP, CASC, etc.'. Together they form a unique fingerprint.

Cite this