TPTP
From MaRDI portal
Software:16327
swMATH4143MaRDI QIDQ16327FDOQ16327
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Title not available (Why is that?)
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
- Advances in Artificial Intelligence – SBIA 2004
- Connection tableau calculi with disjunctive constraints
- Building proofs or counterexamples by analogy in a resolution framework
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Mathematical applications of inductive logic programming
- On using ground joinable equations in equational theorem proving
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- The TPTP problem library
- Title not available (Why is that?)
- KI 2004: Advances in Artificial Intelligence
- Mechanizing Mathematical Reasoning
- Theory reasoning in connection calculi
- Ordered tableaux: extensions and applications
- Title not available (Why is that?)
- Foundations of Information and Knowledge Systems
- Automated Deduction – CADE-20
- Title not available (Why is that?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated Reasoning with Analytic Tableaux and Related Methods
- Octopus: combining learning and parallel search
- Predicting and detecting symmetries in FOL finite model search
- Applying SAT solving in classification of finite algebras
- Things to know when implementing KBO
- The QMLTP problem library for first-order modal logics
- A domain-specific language for cryptographic protocols based on streams
- Computing finite models by reduction to function-free clause logic
- Solving the \$100 modal logic challenge
- Automated deduction and knowledge management in geometry
- Exploiting parallelism: highly competitive semantic tree theorem prover
- Title not available (Why is that?)
- The ILTP problem library for intuitionistic logic
- A Focused Sequent Calculus for Higher-Order Logic
- Computing answers with model elimination
- Constraint solving for proof planning
- Subsumption demodulation in first-order theorem proving
- Controlled integration of the cut rule into connection tableau calculi
- IeanCOP: lean connection-based theorem proving
- Symmetric blocking
- Experiments in the heuristic use of past proof experience
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Efficient encodings of first-order Horn formulas in equational logic
- Subgoal alternation in model elimination
- Automated Reasoning
- Automated Reasoning
- Ground joinability and connectedness in the superposition calculus
- Logic for Programming, Artificial Intelligence, and Reasoning
- \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
- Integration of automated and interactive theorem proving in ILF
- Theorem proving as constraint solving with coherent logic
- Automated Reasoning
- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- The ILLTP library for intuitionistic linear logic
- The design of the CADE-13 ATP system competition
- A Powerful Technique to Eliminate Isomorphism in Finite Model Search
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Linear and unit-resulting refutations for Horn theories
- Some group theoretic examples with completion theorem provers
- Integrating simplex with tableaux
- Herbrand constructivization for automated intuitionistic theorem proving
- Faster, higher, stronger: E 2.3
- GKC: a reasoning system for large knowledge bases
- A scalable module system
- Scavenger 0.1: a theorem prover based on conflict resolution
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- Satallax: An Automatic Higher-Order Prover
- The Relative Power of Semantics and Unification
- HOL Based First-Order Modal Logic Provers
- Computing Tiny Clause Normal Forms
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- MaLeS: a framework for automatic tuning of automated theorem provers
- Mechanizing a process algebra for network protocols
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- SOLAR: An automated deduction system for consequence finding
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Mathematical Knowledge Management
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Theorem Proving in Higher Order Logics
- Combining and automating classical and non-classical logics in classical higher-order logics
- Computer supported mathematics with \(\Omega\)MEGA
- Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings
- Combined reasoning by automated cooperation
- Lightweight relevance filtering for machine-generated resolution problems
- On the practical value of different definitional translations to normal form
- Invariant and type inference for matrices
- Title not available (Why is that?)
This page was built for software: TPTP
