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
- Model Finding for Recursive Functions in SMT
- A proof system for graph (non)-isomorphism verification
- Automating Induction with an SMT Solver
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
- Finding proofs in Tarskian geometry
- Automatic Proof and Disproof in Isabelle/HOL
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- Title not available (Why is that?)
- 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
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
- A heuristic prover for real inequalities
- Mechanizing a process algebra for network protocols
- Semi-intelligible Isar proofs from machine-generated proofs
- MaSh: Machine Learning for Sledgehammer
- 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
- Sledgehammer: Judgement Day
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Extended Conscriptions Algebraically
- A deontic logic reasoning infrastructure
- One Logic to Use Them All
- Algebras for iteration and infinite computations
- Reducing higher-order theorem proving to a sequence of SAT problems
- Relational characterisations of paths
- PRocH: Proof Reconstruction for HOL Light
- 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
- Random Forests for Premise Selection
- Closure, Properties and Closure Properties of Multirelations
- 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
- Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
- Verification and code generation for invariant diagrams in Isabelle
- Stone Relation Algebras
- ATP and presentation service for Mizar formalizations
- Hipster: Integrating Theory Exploration in a Proof Assistant
- 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 proof strategy language and proof script generation for Isabelle/HOL
- 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
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Mechanizing the Metatheory of Sledgehammer
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
- Theorem proving as constraint solving with coherent logic
- Encoding Monomorphic and Polymorphic Types
- In praise of algebra
- A Heuristic Prover for Real Inequalities
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Challenges and Experiences in Managing Large-Scale Proofs
- More SPASS with Isabelle
- Higher-Order Modal Logics: Automation and Applications
- Superposition for Bounded Domains
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
- Computer-Supported Analysis of Arguments in Climate Engineering
- Automated Reasoning in Higher-Order Regular Algebra
- An algebraic approach to multirelations and their properties
- Hammering towards QED
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- A Decision Procedure for (Co)datatypes in SMT Solvers
- Mining State-Based Models from Proof Corpora
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Extracting verified decision procedures: DPLL and Resolution
- 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
- Certification of nonclausal connection tableaux proofs
- Cooperating Proof Attempts
- Computer-Supported Exploration of a Categorical Axiomatization of Modeloids
- Automating Change of Representation for Proofs in Discrete Mathematics
- Extensional higher-order paramodulation in Leo-III
- Title not available (Why is that?)
- Unifying theories of reactive design contracts
- Towards a UTP Semantics for Modelica
- Towards satisfiability modulo parametric bit-vectors
This page was built for software: Sledgehammer
