The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

DOI10.1007/s10817-009-9143-8zbMath1185.68636OpenAlexW1573992413MaRDI QIDQ2655326

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9143-8

zbMATH Keywords

ATP system evaluation TPTP

Mathematics Subject Classification ID

Related Items

Formalizing Some “Small” Finite Models of Projective Geometry in Coq, Automated generation of illustrated proofs in geometry and beyond, Termination Tools in Ordered Completion, Cut-elimination for quantified conditional logic, The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema, MaLeS: a framework for automatic tuning of automated theorem provers, The higher-order prover \textsc{Leo}-II, Semi-intelligible Isar proofs from machine-generated proofs, Mechanizing a process algebra for network protocols, A Polymorphic Vampire, From informal to formal proofs in Euclidean geometry, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, Formal Logic Definitions for Interchange Languages, LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, Eliminating models during model elimination, History and Prospects for First-Order Automated Deduction, Automated Reasoning in the Wild, SMTtoTPTP – A Converter for Theorem Proving Formats, Quantifier-Free Equational Logic and Prime Implicate Generation, Cooperating Proof Attempts, Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses, Beagle – A Hierarchic Superposition Theorem Prover, System Description: E.T. 0.1, Playing with AVATAR, Exploring Theories with a Model-Finding Assistant, Lingva: Generating and Proving Program Properties Using Symbol Elimination, Integrating Simplex with Tableaux, Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics, Multi-completion with termination tools, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, Simulating Dynamic Systems Using Linear Time Calculus Theories, Automated reasoning with restricted intensional sets, On the generation of quantified lemmas, Algorithmic introduction of quantified cuts, Automated theory exploration for interactive theorem proving: an introduction to the Hipster system, Proof certificates in PVS, Solving quantified linear arithmetic by counterexample-guided instantiation, Embedding and automating conditional logics in classical higher-order logic, Constraint solving for finite model finding in SMT solvers, Symmetric blocking, The OWL reasoner evaluation (ORE) 2015 competition report, The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0, Contradiction separation based dynamic multi-clause synergized automated deduction, First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Proofs and Reconstructions, Random Forests for Premise Selection, Incremental variable splitting, Higher-Order Modal Logics: Automation and Applications, Automated inference of finite unsatisfiability, Encoding Monomorphic and Polymorphic Types, First-order automated reasoning with theories: when deduction modulo theory meets practice, Symbolic backward reachability with effectively propositional logic. Application to security policy analysis, Automated Constructivization of Proofs, The CADE-26 automated theorem proving system competition – CASC-26, Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1, The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9, The CADE-27 Automated theorem proving System Competition – CASC-27, The jobs puzzle: Taking on the challenge via controlled natural language processing, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, (Dual) Hoops Have Unique Halving, Toward a Procedure for Data Mining Proofs, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Planning with Effectively Propositional Logic, The Relative Power of Semantics and Unification, Partiality and recursion in interactive theorem provers – an overview, A light-weight integration of automated and interactive theorem proving, Using Mixture of Experts Method in Combining Search-Guiding Heuristics for Theorem Proving, Interpolation and Symbol Elimination in Vampire, Premise Selection in the Naproche System, Specifying and Verifying Organizational Security Properties in First-Order Logic, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), Machine learning guidance for connection tableaux, Experimenting with Deduction Modulo, Heaps and Data Structures: A Challenge for Automated Provers, Sort It Out with Monotonicity, Sine Qua Non for Large Theory Reasoning, System Description: SPASS-FD, On Transfinite Knuth-Bendix Orders, Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions, Blocking and other enhancements for bottom-up model generation methods, Solving quantifier-free first-order constraints over finite sets and binary relations, SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment, Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems, nanoCoP: A Non-clausal Connection Prover, Selecting the Selection, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Effective Normalization Techniques for HOL, Finding Finite Models in Multi-sorted First-Order Logic, Agent-Based HOL Reasoning, Extending SMT solvers to higher-order logic, Induction in saturation-based proof search, Certified equational reasoning via ordered completion, TPTP, Extending Maximal Completion (Invited Talk), Thousands of Geometric Problems for Geometric Theorem Provers (TGTP), A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs, A Vernacular for Coherent Logic, The 10th IJCAR automated theorem proving system competition – CASC-J10, Reducing higher-order theorem proving to a sequence of SAT problems, Extending Sledgehammer with SMT solvers, Machine learning for first-order theorem proving, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

Cites Work