The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574): Difference between revisions

@@ Property / describes a project that uses @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CSPLib
@@ Property / describes a project that uses: CSPLib / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMTtoTPTP
@@ Property / describes a project that uses: SMTtoTPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+IDV
@@ Property / describes a project that uses: IDV / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-017-9407-7
+Normal rank
@@ Property / OpenAlex ID @@
+W2588018425
@@ Property / OpenAlex ID: W2588018425 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075241
@@ Property / cites work: Q3075241 / rank @@
+Normal rank
@@ Property / cites work @@
+SMTtoTPTP – A Converter for Theorem Proving Formats
+Normal rank
@@ Property / cites work @@
+Quantified multimodal logics in simple type theory
+Normal rank
@@ Property / cites work @@
+Combined reasoning by automated cooperation
@@ Property / cites work: Combined reasoning by automated cooperation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5282959
@@ Property / cites work: Q5282959 / rank @@
+Normal rank
@@ Property / cites work @@
+A learning-based fact selector for Isabelle/HOL
@@ Property / cites work: A learning-based fact selector for Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+The ILTP problem library for intuitionistic logic
@@ Property / cites work: The ILTP problem library for intuitionistic logic / rank @@
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+Automated Reasoning in Kleene Algebra
@@ Property / cites work: Automated Reasoning in Kleene Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Q2749862
@@ Property / cites work: Q2749862 / rank @@
+Normal rank
@@ Property / cites work @@
+Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
+Normal rank
@@ Property / cites work @@
+A First Class Boolean Sort in First-Order Theorem Proving and TPTP
+Normal rank
@@ Property / cites work @@
+Non-Horn clause logic programming without contrapositives
+Normal rank
@@ Property / cites work @@
+leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
+Normal rank
@@ Property / cites work @@
+Seventy-five problems for testing automatic theorem provers
+Normal rank
@@ Property / cites work @@
+Automated deduction in von Neumann-Bernays-Gödel set theory
+Normal rank
@@ Property / cites work @@
+The IJCAR ATP system competition
@@ Property / cites work: The IJCAR ATP system competition / rank @@
+Normal rank
@@ Property / cites work @@
+TPTP, TSTP, CASC, etc.
@@ Property / cites work: TPTP, TSTP, CASC, etc. / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+The TPTP World – Infrastructure for Automated Reasoning
+Normal rank
@@ Property / cites work @@
+The TPTP Typed First-Order Form with Arithmetic
@@ Property / cites work: The TPTP Typed First-Order Form with Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Using the TPTP Language for Writing Derivations and Finite Interpretations
+Normal rank
@@ Property / cites work @@
+Q5486135
@@ Property / cites work: Q5486135 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library. CNF release v1. 2. 1
@@ Property / cites work: The TPTP problem library. CNF release v1. 2. 1 / rank @@
+Normal rank
@@ Property / cites work @@
+Evaluating general purpose automated theorem proving systems
+Normal rank
@@ Property / cites work @@
+An Interactive Derivation Viewer
@@ Property / cites work: An Interactive Derivation Viewer / rank @@
+Normal rank
@@ Property / cites work @@
+ATP and presentation service for Mizar formalizations
+Normal rank
@@ Property / cites work @@
+MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
+Normal rank
@@ Property / cites work @@
+Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
+Normal rank
@@ Property / cites work @@
+System for Automated Deduction (SAD): A Tool for Proof Verification
+Normal rank
@@ Property / cites work @@
+Problems and Experiments for and with Automated Theorem-Proving Programs
+Normal rank