Sledgehammer
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Tool-Based Verification of a Relational Vertex Coloring Program
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- A framework for developing stand-alone certifiers
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Flexible proof production in an industrial-strength SMT solver
- 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
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- Superposition with lambdas
- Certification of nonclausal connection tableaux proofs
- On the fine-structure of regular algebra
- SErAPIS
- The CADE-26 automated theorem proving system competition -- CASC-26
- A proof system for graph (non)-isomorphism verification
- Automating Induction with an SMT Solver
- Finding proofs in Tarskian geometry
- Extensional higher-order paramodulation in Leo-III
- Automating Change of Representation for Proofs in Discrete Mathematics
- Closure, properties and closure properties of multirelations
- Formalizing axiomatic systems for propositional logic in Isabelle/HOL
- Unifying theories of reactive design contracts
- Automating theorem proving with SMT
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Towards satisfiability modulo parametric bit-vectors
- 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 heuristic prover for real inequalities
- Mechanizing a process algebra for network protocols
- Semi-intelligible Isar proofs from machine-generated proofs
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- A heuristic prover for real inequalities
- Formalizing geometric algebra in Lean
- Foreword to the special focus on formal proofs for mathematics and computer science
- Contextual Natural Deduction
- Superposition for bounded domains
- Proofs and reconstructions
- Random forests for premise selection
- Relation-algebraic verification of Prim's minimum spanning tree algorithm
- Mining the Archive of Formal Proofs
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Mining state-based models from proof corpora
- An algebraic approach to computations with progress
- Computer-supported analysis of arguments in climate engineering
- Verifying minimum spanning tree algorithms with Stone relation algebras
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Reducing higher-order theorem proving to a sequence of SAT problems
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- A combinator-based superposition calculus for higher-order logic
- From informal to formal proofs in Euclidean geometry
- A deontic logic reasoning infrastructure
- Internal guidance for Satallax
- Making higher-order superposition work
- Superposition with lambdas
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Extracting verified decision procedures: DPLL and resolution
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- Algebras for iteration and infinite computations
- Reducing higher-order theorem proving to a sequence of SAT problems
- Extracting a DPLL algorithm
- Automating change of representation for proofs in discrete mathematics (extended version)
- Implementation and evaluation of contextual natural deduction for minimal logic
- An Axiomatic Value Model for Isabelle/UTP
- Relational characterisations of paths
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- ACL2
- HOL-Boogie
- HYBRID
- Isabelle
- LEO-II
- Nitpick
- RelView
- TPS
- Isabelle/HOL
- Isabelle/Isar
- AFRA
- IsaPlanner
- MPTP
- MPTP 0.2
- VAMPIRE
- THF0
- Darwin
- SMT-LIB
- SPASS
- TPTP
- Isar
- SPASS+T
- Prover9
- z3
- HOL
- Saoithin
- Isabelle/jEdit
- PIDE
- CeTA
- HOL Light
- UTP2
- E-Darvin
This page was built for software: Sledgehammer
