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