TPTP, TSTP, CASC, etc.

Geoff Sutcliffe

doi:10.1007/978-3-540-74510-5_4

TPTP, TSTP, CASC, etc.

Geoff Sutcliffe

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

12 Scopus citations

Abstract

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 language	English (US)
Title of host publication	Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings
Publisher	Springer Verlag
Pages	6-22
Number of pages	17
ISBN (Print)	9783540745099
DOIs	https://doi.org/10.1007/978-3-540-74510-5_4
State	Published - Jan 1 2007
Event	2nd International Symposium on Computer Science in Russia, CSR 2007 - Ekaterinburg, Russian Federation Duration: Sep 3 2007 → Sep 7 2007

Publication series

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

Other

Other	2nd International Symposium on Computer Science in Russia, CSR 2007
Country	Russian Federation
City	Ekaterinburg
Period	9/3/07 → 9/7/07

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-74510-5_4

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

Cite this

Sutcliffe, G. (2007). TPTP, TSTP, CASC, etc. In Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings (pp. 6-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4649 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74510-5_4

TPTP, TSTP, CASC, etc. / Sutcliffe, Geoff.

Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings. Springer Verlag, 2007. p. 6-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4649 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sutcliffe, G 2007, TPTP, TSTP, CASC, etc. in Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4649 LNCS, Springer Verlag, pp. 6-22, 2nd International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russian Federation, 9/3/07. https://doi.org/10.1007/978-3-540-74510-5_4

Sutcliffe G. TPTP, TSTP, CASC, etc. In Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings. Springer Verlag. 2007. p. 6-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-74510-5_4

@inproceedings{44b885d763064527b815c8a6e116a8d1,

title = "TPTP, TSTP, CASC, etc.",

abstract = "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.",

author = "Geoff Sutcliffe",

year = "2007",

month = jan,

day = "1",

doi = "10.1007/978-3-540-74510-5_4",

language = "English (US)",

isbn = "9783540745099",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "6--22",

booktitle = "Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings",

note = "2nd International Symposium on Computer Science in Russia, CSR 2007 ; Conference date: 03-09-2007 Through 07-09-2007",

}

TY - GEN

T1 - TPTP, TSTP, CASC, etc.

AU - Sutcliffe, Geoff

PY - 2007/1/1

Y1 - 2007/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=37249087160&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=37249087160&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-74510-5_4

DO - 10.1007/978-3-540-74510-5_4

M3 - Conference contribution

AN - SCOPUS:37249087160

SN - 9783540745099

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 6

EP - 22

BT - Computer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings

PB - Springer Verlag

T2 - 2nd International Symposium on Computer Science in Russia, CSR 2007

Y2 - 3 September 2007 through 7 September 2007

ER -