TPTP, TSTP, CASC, etc

Geoff Sutcliffe

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

Back

Book chapter

TPTP, TSTP, CASC, etc

Geoff Sutcliffe

Computer Science – Theory and Applications, pp.6-22

Lecture Notes in Computer Science, Springer Berlin Heidelberg

DOI: https://doi.org/10.1007/978-3-540-74510-5_4

Abstract

Automate Reasoning

Automate Theorem Prove

Solution Library

Inference Step

Interesting Theorem

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.

Metrics

11 Record Views

Details

Title: TPTP, TSTP, CASC, etc
Creators: Geoff Sutcliffe - University of Miami, USA
Publication Details: Computer Science – Theory and Applications, pp.6-22
Series: Lecture Notes in Computer Science
Publisher: Springer Berlin Heidelberg; Berlin, Heidelberg
ISSN: 1611-3349
Academic Unit: Leadership Department; College of A&S; A&S - Computer Science
Language: English
Resource Type: Book chapter
Record Identifier: 991031598591402976