swMATH10133MaRDI QIDQ22101FDOQ22101
Author name not available (Why is that?)
Official website: http://deepthought.ttu.ee/it/gandalf/
Cited In (45)
- Extending Sledgehammer with SMT solvers
- Optimized encodings of fragments of type theory in first-order logic
- Proof search and proof check for equational and inductive theorems.
- Title not available (Why is that?)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Title not available (Why is that?)
- Optimized encodings of fragments of type theory in first order logic
- Exploiting parallelism: highly competitive semantic tree theorem prover
- Complete integer decision procedures as derived rules in HOL
- Efficiently checking propositional refutations in HOL theorem provers
- Providing a formal linkage between MDG and HOL
- Title not available (Why is that?)
- Modular SMT proofs for fast reflexive checking inside Coq
- Automated Reasoning with Analytic Tableaux and Related Methods
- External rewriting for skeptical proof assistants
- THEO
- Paradox
- E-MaLeS 1.1
- Ivy
- PROSPER
- Automated proof construction in type theory using resolution
- Title not available (Why is that?)
- OMEGA
- TRAMP
- HERBY
- PrHERBY
- Robbins Conjecture
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Automated Reasoning
- The HOL Light theory of Euclidean space
- Frontiers of Combining Systems
- Integrating a SAT solver with an LCF-style theorem prover
- Tools and Algorithms for the Construction and Analysis of Systems
- More SPASS with Isabelle
- Automated Reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Automation for interactive proof: first prototype
- Hammering towards QED
- Metis
- Automated Technology for Verification and Analysis
- Source-Level Proof Reconstruction for Interactive Theorem Proving
This page was built for software: Gandalf
