Sledgehammer
From MaRDI portal
Software:19106
swMATH7047MaRDI QIDQ19106FDOQ19106
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Tool-Based Verification of a Relational Vertex Coloring Program
- Superposition with lambdas
- A framework for developing stand-alone certifiers
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- On the fine-structure of regular algebra
- A proof system for graph (non)-isomorphism verification
- Automating Induction with an SMT Solver
- Finding proofs in Tarskian geometry
- Closure, properties and closure properties of multirelations
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Formalization of the resolution calculus for first-order logic
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- A heuristic prover for real inequalities
- Mechanizing a process algebra for network protocols
- Semi-intelligible Isar proofs from machine-generated proofs
- A heuristic prover for real inequalities
- Superposition for bounded domains
- Relation-algebraic verification of Prim's minimum spanning tree algorithm
- Random forests for premise selection
- Computer-supported analysis of arguments in climate engineering
- Mining the Archive of Formal Proofs
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Title not available (Why is that?)
- Verifying minimum spanning tree algorithms with Stone relation algebras
- An algebraic approach to computations with progress
- Reliable reconstruction of fine-grained proofs in a proof assistant
- A combinator-based superposition calculus for higher-order logic
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- A deontic logic reasoning infrastructure
- Algebras for iteration and infinite computations
- Reducing higher-order theorem proving to a sequence of SAT problems
- Relational characterisations of paths
- Soundness and completeness proofs by coinductive methods
- A verified SAT solver framework with learn, forget, restart, and incrementality
- CoSMed: a confidentiality-verified social media platform
- Introduction to ``Milestones in interactive theorem proving
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Encoding monomorphic and polymorphic types
- Mechanizing the metatheory of Sledgehammer
- A formally verified proof of the central limit theorem
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- A learning-based fact selector for Isabelle/HOL
- Sledgehammer: judgement day
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Automated and human proofs in general mathematics: an initial comparison
- Challenges and experiences in managing large-scale proofs
- MaSh: machine learning for Sledgehammer
- Higher-order modal logics: automation and applications
- Verification and code generation for invariant diagrams in Isabelle
- Interactive theorem proving from the perspective of Isabelle/Isar
- ATP and presentation service for Mizar formalizations
- Extended conscriptions algebraically
- An algebraic framework for minimum spanning tree problems
- Learning-assisted theorem proving with millions of lemmas
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- A proof strategy language and proof script generation for Isabelle/HOL
- One logic to use them all
- Infinite executions of lazy and strict computations
- A Hierarchy of Algebras for Boolean Subsets
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- The HOL Light theory of Euclidean space
- Theorem proving as constraint solving with coherent logic
- In praise of algebra
- More SPASS with Isabelle
- Model finding for recursive functions in SMT
- Automatic proof and disproof in Isabelle/HOL
- PRocH: proof reconstruction for HOL Light
- Automated Reasoning in Higher-Order Regular Algebra
- Hipster: integrating theory exploration in a proof assistant
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- AUTO2, a saturation-based heuristic prover for higher-order logic
- An algebraic approach to multirelations and their properties
- Hammering towards QED
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Stone relation algebras
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Flexible proof production in an industrial-strength SMT solver
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- The CADE-26 automated theorem proving system competition -- CASC-26
- Certification of nonclausal connection tableaux proofs
- Automating Change of Representation for Proofs in Discrete Mathematics
- Extensional higher-order paramodulation in Leo-III
- Automating theorem proving with SMT
- Title not available (Why is that?)
- Unifying theories of reactive design contracts
- Towards satisfiability modulo parametric bit-vectors
- Contextual Natural Deduction
- Formalizing geometric algebra in Lean
- Foreword to the special focus on formal proofs for mathematics and computer science
This page was built for software: Sledgehammer
