Cited in
(45)- Optimized encodings of fragments of type theory in first-order logic
- Extending Sledgehammer with SMT solvers
- Proof search and proof check for equational and inductive theorems.
- scientific article; zbMATH DE number 1696826 (Why is no real title available?)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- scientific article; zbMATH DE number 2086953 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 1614692 (Why is no real title available?)
- THEO
- Paradox
- Ivy
- PROSPER
- OMEGA
- TRAMP
- HERBY
- PrHERBY
- Robbins Conjecture
- External rewriting for skeptical proof assistants
- Modular SMT proofs for fast reflexive checking inside Coq
- Metis
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated proof construction in type theory using resolution
- E-MaLeS 1.1
- scientific article; zbMATH DE number 1566502 (Why is no real title available?)
- 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
- More SPASS with Isabelle
- Tools and Algorithms for the Construction and Analysis of Systems
- Automated Reasoning
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Automation for interactive proof: first prototype
- scientific article; zbMATH DE number 2086601 (Why is no real title available?)
- scientific article; zbMATH DE number 1852162 (Why is no real title available?)
- Hammering towards QED
- Automated Technology for Verification and Analysis
- Source-Level Proof Reconstruction for Interactive Theorem Proving
This page was built for software: Gandalf
