TPTP
From MaRDI portal
Software:16327
swMATH4143MaRDI QIDQ16327FDOQ16327
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- 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
- nanoCoP: A Non-clausal Connection Prover
- System Description: GAPT 2.0
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- The Relative Power of Semantics and Unification
- HOL Based First-Order Modal Logic Provers
- Computing Tiny Clause Normal Forms
- The 481 Ways to Split a Clause and Deal with Propositional Variables
- Title not available (Why is that?)
- 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
- Beagle – A Hierarchic Superposition Theorem Prover
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
- SMTtoTPTP – A Converter for Theorem Proving Formats
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Lingva: Generating and Proving Program Properties Using Symbol Elimination
- 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
- PRocH: Proof Reconstruction for HOL Light
- Invariant and type inference for matrices
- Citius altius fortius
- Title not available (Why is that?)
- Title not available (Why is that?)
- Evaluating general purpose automated theorem proving systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Panoptes
- The CADE-22 automated theorem proving system competition -- CASC-22
- Automated reasoning and presentation support for formalizing mathematics in MizAR
- Interpolation and symbol elimination in Vampire
- Title not available (Why is that?)
- Title not available (Why is that?)
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Sine qua non for large theory reasoning
- EPR-based bounded model checking at word level
- ILF-SETHEO
- Model evolution with equality -- revised and implemented
- Loop Analysis by Quantification over Iterations
- CODE: A powerful prover for problems of condensed detachment
- TPS: A theorem-proving system for classical type theory
- MPTP-motivation, implementation, first experiments
- Automated Deduction – CADE-20
- HOL(y)Hammer: online ATP service for HOL Light
- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
- MPTP 0.2: Design, implementation, and initial experiments
- SAD as a mathematical assistant -- how should we go from here to there?
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- The model evolution calculus as a first-order DPLL method
- Translating higher-order clauses to first-order clauses
- System Description: E 1.8
- Model elimination and connection tableau procedures
- Automated Reasoning Service for HOL Light
- Showing Invariance Compositionally for a Process Algebra for Network Protocols
- MædMax: a maximal ordered completion tool
- On Logic Embeddings and Gödel’s God
- More SPASS with Isabelle
- Playing in the grey area of proofs
- Higher-Order Modal Logics: Automation and Applications
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Hammer for Coq: automation for dependent type theory
- Thousands of geometric problems for geometric theorem provers (TGTP)
- LEO-II and Satallax on the Sledgehammer test bench
- ATPboost: learning premise selection in binary setting with ATP feedback
- The higher-order prover Leo-III
- Proof Systems for Effectively Propositional Logic
- Automatic acquisition of search control knowledge from multiple proof attempts.
- Efficient model generation through compilation.
- Blocking and other enhancements for bottom-up model generation methods
- Old or heavy? Decaying gracefully with age/weight shapes
This page was built for software: TPTP
