Gandalf
From MaRDI portal
Software:22101
swMATH10133MaRDI QIDQ22101FDOQ22101
Author name not available (Why is that?)
Cited In (35)
- 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
- E-MaLeS 1.1
- Automated proof construction in type theory using resolution
- Title not available (Why is that?)
- 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
- Automated Technology for Verification and Analysis
- Source-Level Proof Reconstruction for Interactive Theorem Proving
This page was built for software: Gandalf