Pages that link to "Item:Q2655326"
From MaRDI portal
The following pages link to The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326):
Displaying 50 items.
- TPTP (Q16327) (← links)
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- Multi-completion with termination tools (Q352956) (← links)
- Algorithmic introduction of quantified cuts (Q402115) (← links)
- Incremental variable splitting (Q429591) (← links)
- Automated inference of finite unsatisfiability (Q438540) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Symmetric blocking (Q897931) (← links)
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (Q1687709) (← links)
- Proof certificates in PVS (Q1687741) (← links)
- Solving quantified linear arithmetic by counterexample-guided instantiation (Q1688537) (← links)
- The OWL reasoner evaluation (ORE) 2015 competition report (Q1694573) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- Embedding and automating conditional logics in classical higher-order logic (Q1935597) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- Eliminating models during model elimination (Q2142079) (← links)
- Contradiction separation based dynamic multi-clause synergized automated deduction (Q2198231) (← links)
- First-order automated reasoning with theories: when deduction modulo theory meets practice (Q2209546) (← links)
- Blocking and other enhancements for bottom-up model generation methods (Q2303239) (← links)
- Solving quantifier-free first-order constraints over finite sets and binary relations (Q2303241) (← links)
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment (Q2303255) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Induction in saturation-based proof search (Q2305434) (← links)
- Certified equational reasoning via ordered completion (Q2305436) (← links)
- Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Machine learning for first-order theorem proving (Q2351414) (← links)
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry (Q2354917) (← links)
- Cut-elimination for quantified conditional logic (Q2363418) (← links)
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (Q2364696) (← links)
- On the generation of quantified lemmas (Q2417949) (← links)
- Symbolic backward reachability with effectively propositional logic. Application to security policy analysis (Q2441771) (← links)
- From informal to formal proofs in Euclidean geometry (Q2631958) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- Automated reasoning with restricted intensional sets (Q2666960) (← links)
- Race Against the Teens – Benchmarking Mechanized Math on Pre-university Problems (Q2817922) (← links)
- nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
- Selecting the Selection (Q2817931) (← links)
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (Q2817933) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Finding Finite Models in Multi-sorted First-Order Logic (Q2818025) (← links)
- Agent-Based HOL Reasoning (Q2819202) (← links)
- Simulating Dynamic Systems Using Linear Time Calculus Theories (Q2931258) (← links)
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation (Q2964455) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
