The following pages link to TPTP (Q16327):
Displaying 50 items.
- 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)
- A scalable module system (Q391632) (← links)
- Algorithmic introduction of quantified cuts (Q402115) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Incremental variable splitting (Q429591) (← links)
- Automated inference of finite unsatisfiability (Q438540) (← links)
- Conjecture synthesis for inductive theories (Q438543) (← links)
- MPTP-motivation, implementation, first experiments (Q556682) (← links)
- Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 -- May 1, 2010. Revised selected papers (Q610791) (← links)
- Internal axioms for domain semirings (Q627202) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- An erratum for some errata to ATP problems (Q679255) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Octopus: combining learning and parallel search (Q861370) (← links)
- Predicting and detecting symmetries in FOL finite model search (Q861703) (← links)
- Things to know when implementing KBO (Q861708) (← links)
- Applying SAT solving in classification of finite algebras (Q862393) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- MPTP 0.2: Design, implementation, and initial experiments (Q877826) (← links)
- The ILTP problem library for intuitionistic logic (Q877897) (← links)
- Symmetric blocking (Q897931) (← links)
- Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings (Q926451) (← links)
- Combined reasoning by automated cooperation (Q946572) (← links)
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings (Q951681) (← links)
- Hashing and canonicalizing Notation 3 graphs (Q988582) (← links)
- A domain-specific language for cryptographic protocols based on streams (Q1001891) (← links)
- Lightweight relevance filtering for machine-generated resolution problems (Q1006731) (← links)
- Computing finite models by reduction to function-free clause logic (Q1006733) (← links)
- Solving the \$100 modal logic challenge (Q1006738) (← links)
- Labelled splitting (Q1037396) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- First order Stålmarck. Universal lemmas through branch merges (Q1040785) (← links)
- Theory reasoning in connection calculi (Q1276499) (← links)
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (Q1340966) (← links)
- Controlled integration of the cut rule into connection tableau calculi (Q1344875) (← links)
- A disjunctive positive refinement of model elimination and its application to subsumption deletion (Q1369080) (← links)
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference (Q1373304) (← links)
- Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
- Computing answers with model elimination (Q1402748) (← links)
- IeanCOP: lean connection-based theorem proving (Q1404981) (← links)
