Gandalf

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