The following pages link to Gandalf (Q22101):
Displaying 35 items.
- Providing a formal linkage between MDG and HOL (Q878110) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- Automated proof construction in type theory using resolution (Q1868508) (← links)
- External rewriting for skeptical proof assistants (Q1868511) (← links)
- The HOL Light theory of Euclidean space (Q1945903) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Automation for interactive proof: first prototype (Q2432769) (← links)
- (Q2701741) (← links)
- (Q2723415) (← links)
- (Q2767093) (← links)
- (Q2848690) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs (Q3498463) (← links)
- Source-Level Proof Reconstruction for Interactive Theorem Proving (Q3523178) (← links)
- Complete Integer Decision Procedures as Derived Rules in HOL (Q3559760) (← links)
- Optimized encodings of fragments of type theory in first-order logic (Q4228072) (← links)
- Optimized encodings of fragments of type theory in first order logic (Q4647585) (← links)
- (Q4737135) (← links)
- (Q4737561) (← links)
- (Q4787234) (← links)
- Exploiting parallelism: highly competitive semantic tree theorem prover (Q4823345) (← links)
- E-MaLeS 1.1 (Q4928455) (← links)
- Hammering towards QED (Q5195271) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Automated Reasoning (Q5307066) (← links)
- Automated Reasoning (Q5307074) (← links)
- Automated Technology for Verification and Analysis (Q5394196) (← links)
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case (Q5428267) (← links)
- Automated Reasoning with Analytic Tableaux and Related Methods (Q5479279) (← links)
- Frontiers of Combining Systems (Q5491905) (← links)
- Tools and Algorithms for the Construction and Analysis of Systems (Q5899057) (← links)
- Automated Deduction – CADE-19 (Q5900725) (← links)
