The following pages link to Sledgehammer (Q19106):
Displaying 50 items.
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Mechanizing a process algebra for network protocols (Q287372) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- An algebraic approach to computations with progress (Q299188) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Programming and automating mathematics in the Tarski-Kleene hierarchy (Q406433) (← links)
- Verification and code generation for invariant diagrams in Isabelle (Q478381) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- An algebraic approach to multirelations and their properties (Q516032) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Algebras for iteration and infinite computations (Q715050) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL (Q832723) (← links)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- A formally verified proof of the central limit theorem (Q1694568) (← links)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (Q1694574) (← links)
- Strategy analysis of non-consequence inference with Euler diagrams (Q1711501) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- An algebraic framework for minimum spanning tree problems (Q1786562) (← links)
- A Coq tactic for equality learning in linear arithmetic (Q1791149) (← links)
- Superposition with datatypes and codatatypes (Q1799098) (← links)
- Datatypes with shared selectors (Q1799121) (← links)
- An abstraction-refinement framework for reasoning with large theories (Q1799131) (← links)
- Left omega algebras and regular equations (Q1931903) (← links)
- In praise of algebra (Q1941861) (← links)
- The HOL Light theory of Euclidean space (Q1945903) (← links)
- ATP and presentation service for Mizar formalizations (Q1945905) (← links)
- Verifying minimum spanning tree algorithms with Stone relation algebras (Q1994364) (← links)
- Unifying theories of reactive design contracts (Q2007732) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (Q2031406) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Integration of formal proof into unified assurance cases with Isabelle/SACM (Q2065527) (← links)
- A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL (Q2128791) (← links)
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (Q2128804) (← links)
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search (Q2142075) (← links)
- Certification of nonclausal connection tableaux proofs (Q2180504) (← links)
