The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
type: Item
instance of: scholarly article
title: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
zbMATH Open document ID: 1425.68381
author: Geoff Sutcliffe
published in: Journal of Automated Reasoning
publication date: 2018-02-02T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6833659
zbMATH Keywords: TPTP
zbMATH Keywords: ATP system evaluation
zbMATH Keywords: ATP standards and tools
describes a project that uses: ileanCoP
describes a project that uses: MPTP 0.2
describes a project that uses: SMT-LIB
describes a project that uses: SAD
describes a project that uses: QBFEVAL
describes a project that uses: ILTP
describes a project that uses: SATLIB
describes a project that uses: leanCoP
describes a project that uses: MaLARea
describes a project that uses: Flyspeck
describes a project that uses: FOOL
describes a project that uses: OTTER
describes a project that uses: TPTP
describes a project that uses: CSPLib
describes a project that uses: Sledgehammer
describes a project that uses: SMTtoTPTP
describes a project that uses: IDV
MaRDI profile type: Publication
full work available at URL: s10817-017-9407-7
OpenAlex ID: W2588018425
cites work: Q3075241
cites work: SMTtoTPTP – A Converter for Theorem Proving Formats
cites work: Quantified multimodal logics in simple type theory
cites work: Combined reasoning by automated cooperation
cites work: Q5282959
cites work: A learning-based fact selector for Isabelle/HOL
cites work: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
cites work: Sledgehammer: Judgement Day
cites work: Automated Reasoning
cites work: The ILTP problem library for intuitionistic logic
cites work: MPTP 0.2: Design, implementation, and initial experiments
cites work: Automated Reasoning in Kleene Algebra
cites work: SATLIB: An online resource for research on SAT
cites work: Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
cites work: A First Class Boolean Sort in First-Order Theorem Proving and TPTP
cites work: Non-Horn clause logic programming without contrapositives
cites work: leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
cites work: Seventy-five problems for testing automatic theorem provers
cites work: Automated deduction in von Neumann-Bernays-Gödel set theory
cites work: The IJCAR ATP system competition
cites work: TPTP, TSTP, CASC, etc.
cites work: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
cites work: The TPTP World – Infrastructure for Automated Reasoning
cites work: The TPTP Typed First-Order Form with Arithmetic
cites work: Using the TPTP Language for Writing Derivations and Finite Interpretations
cites work: Q5486135
cites work: The TPTP problem library. CNF release v1. 2. 1
cites work: Evaluating general purpose automated theorem proving systems
cites work: An interactive derivation viewer
cites work: ATP and presentation service for Mizar formalizations
cites work: MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
cites work: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
cites work: System for Automated Deduction (SAD): A Tool for Proof Verification
cites work: Problems and Experiments for and with Automated Theorem-Proving Programs
DOI: 10.1007/S10817-017-9407-7
Recommended article: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
Recommended article: The TPTP problem library. CNF release v1. 2. 1
Recommended article: The TPTP problem library
Recommended article: THF0 – The Core of the TPTP Language for Higher-Order Logic
Recommended article: The ILTP problem library for intuitionistic logic
Recommended article: Q3150303
Recommended article: Q3075241
Recommended article: The TPTP World – Infrastructure for Automated Reasoning
Recommended article: The theoretical foundations of LPTP (a logic program theorem prover)
Recommended article: Logics in Artificial Intelligence
description: scientific article; zbMATH DE number 6833659