Gandalf

swMATH10133MaRDI QIDQ22101

No author found.

Related Items (35)

Unnamed Item ⋮ More SPASS with Isabelle ⋮ Unnamed Item ⋮ Exploiting parallelism: highly competitive semantic tree theorem prover ⋮ Automated Technology for Verification and Analysis ⋮ Providing a formal linkage between MDG and HOL ⋮ Unnamed Item ⋮ Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The HOL Light theory of Euclidean space ⋮ Automation for interactive proof: first prototype ⋮ Source-Level Proof Reconstruction for Interactive Theorem Proving ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ Unnamed Item ⋮ Complete Integer Decision Procedures as Derived Rules in HOL ⋮ Optimized encodings of fragments of type theory in first order logic ⋮ Frontiers of Combining Systems ⋮ Unnamed Item ⋮ E-MaLeS 1.1 ⋮ Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case ⋮ Extending Sledgehammer with SMT Solvers ⋮ Efficiently checking propositional refutations in HOL theorem provers ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Automated Reasoning with Analytic Tableaux and Related Methods ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Automated Deduction – CADE-19 ⋮ Automated Reasoning ⋮ Automated Reasoning ⋮ Optimized encodings of fragments of type theory in first-order logic ⋮ Hammering towards QED ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Automated proof construction in type theory using resolution ⋮ External rewriting for skeptical proof assistants

This page was built for software: Gandalf