Sledgehammer
From MaRDI portal
Cited in
(only showing first 100 items - show all)- ACL2
- HOL-Boogie
- HYBRID
- Isabelle
- LEO-II
- Nitpick
- Nunchaku
- RelView
- TPS
- Isabelle/HOL
- Isabelle/Isar
- IsaPlanner
- AFRA
- MPTP
- MPTP 0.2
- VAMPIRE
- THF0
- SMT-LIB
- SPASS
- TPTP
- Darwin
- Metis
- Introduction to ``Milestones in interactive theorem proving
- CoSMed: a confidentiality-verified social media platform
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of the resolution calculus for first-order logic
- A deontic logic reasoning infrastructure
- Isar
- SPASS+T
- A formally verified proof of the central limit theorem
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- z3
- Strategy analysis of non-consequence inference with Euler diagrams
- Prover9
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- HOL
- An algebraic framework for minimum spanning tree problems
- A Coq tactic for equality learning in linear arithmetic
- Superposition with datatypes and codatatypes
- Datatypes with shared selectors
- An abstraction-refinement framework for reasoning with large theories
- Saoithin
- UTP2
- PIDE
- Isabelle/jEdit
- HOL Light
- CeTA
- Zenon
- Satallax
- E-Darvin
- Mace4
- MML
- HOCL
- Kodkod
- ArgoCLP
- Left omega algebras and regular equations
- QuickCheck
- veriT
- In praise of algebra
- The HOL Light theory of Euclidean space
- ATP and presentation service for Mizar formalizations
- Verifying minimum spanning tree algorithms with Stone relation algebras
- Unifying theories of reactive design contracts
- Foreword to the special focus on formal proofs for mathematics and computer science
- MaSh
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- LCF
- CLSAT
- versat
- Towards satisfiability modulo parametric bit-vectors
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- CakeML
- StarExec
- A Knuth-Bendix-like ordering for orienting combinator equations
- A combinator-based superposition calculus for higher-order logic
- Theorem proving as constraint solving with coherent logic
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Flexible proof production in an industrial-strength SMT solver
- Leon
- Formalizing geometric algebra in Lean
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- CVC4
- TLAPS
- jEdit
- iProver
- SmallCheck
- leanCoP
- ForTheL
- Certification of nonclausal connection tableaux proofs
- PLT Redex
- KLMLean
- Gandalf
- Relational characterisations of paths
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- E Theorem Prover
- PRocH
This page was built for software: Sledgehammer
