On the public citation graph
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
0 signed · 77 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/3-540-44755-5_7openalex-snapshot
Calculational Reasoning Revisited An Isabelle/Isar Experience
inferredcites →https://doi.org/10.1007/3-540-45949-9openalex-snapshot
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
inferredcites →https://doi.org/10.1007/978-3-540-74591-4_18openalex-snapshot
Source-Level Proof Reconstruction for Interactive Theorem Proving
inferredcites →https://doi.org/10.1007/978-3-642-14203-1_9openalex-snapshot
Sledgehammer: Judgement Day
inferredcites →https://doi.org/10.1007/978-3-642-60858-2_25openalex-snapshot
Tool Support for Logics of Programs
inferredcites →https://doi.org/10.1007/978-94-017-0435-9_4openalex-snapshot
Integrating Automated and Interactive Theorem Proving
inferredcites →https://doi.org/10.1007/bf00248324openalex-snapshot
The foundation of a generic theorem prover
inferredcites →https://doi.org/10.1007/bfb0028402openalex-snapshot
Type classes and overloading in higher-order logic
inferredcites →https://doi.org/10.1007/s10817-007-9085-yopenalex-snapshot
Translating Higher-Order Clauses to First-Order Clauses
inferredcites →https://doi.org/10.1016/0004-3702(93)90083-nopenalex-snapshot
Ontic: A knowledge representation system for mathematics
inferredcites →https://doi.org/10.1016/b978-044450813-3/50008-4openalex-snapshot
Computing Small Clause Normal Forms
inferredcites →https://doi.org/10.1016/b978-044450813-3/50029-1openalex-snapshot
Combining Superposition, Sorts and Splitting
inferredcites →https://doi.org/10.1016/j.entcs.2004.10.027openalex-snapshot
Bounded Model Generation for Isabelle/HOL
inferredcites →https://doi.org/10.1016/j.ic.2005.05.010openalex-snapshot
Automation for interactive proof: First prototype
inferredcites →https://doi.org/10.1016/j.jal.2007.07.004openalex-snapshot
Lightweight relevance filtering for machine-generated resolution problems
inferredcites →https://doi.org/10.1016/s0747-7171(03)00040-3openalex-snapshot
Limited resource strategy in resolution theorem proving
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/978-3-030-28483-1_4openalex-snapshot
SMTCoq: Mixing Automatic and Interactive Proof Technologies
inferred← citeshttps://doi.org/10.1007/978-3-030-79876-5_36openalex-snapshot
The Isabelle/Naproche Natural Language Proof Assistant
inferred← citeshttps://doi.org/10.1007/978-3-031-15791-2_16openalex-snapshot
Automated Kantian Ethics: A Faithful Implementation
inferred← citeshttps://doi.org/10.1007/978-3-031-66676-6_15openalex-snapshot
A Graphical Representation of Verification Proof Plans
inferred← citeshttps://doi.org/10.1007/978-3-032-07021-0_1openalex-snapshot
Hammering Higher Order Set Theory
inferred← citeshttps://doi.org/10.1007/978-3-032-38214-6_1openalex-snapshot
Semantic Alignment Models: A Bridge Between Informal and Formal Mathematics
inferred← citeshttps://doi.org/10.1007/978-3-319-03545-1_17openalex-snapshot
Formalizing Probabilistic Noninterference
inferred← citeshttps://doi.org/10.1007/978-3-319-08970-6_4openalex-snapshot
Implicational Rewriting Tactics in HOL
inferred← citeshttps://doi.org/10.1007/978-3-319-08970-6_8openalex-snapshot
Cardinals in Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/978-3-319-20615-8_1openalex-snapshot
Mining the Archive of Formal Proofs
inferred← citeshttps://doi.org/10.1007/978-3-319-20615-8_15openalex-snapshot
Automating Change of Representation for Proofs in Discrete Mathematics
inferred← citeshttps://doi.org/10.1007/978-3-319-24246-0_16openalex-snapshot
Proofs and Reconstructions
inferred← citeshttps://doi.org/10.1007/978-3-319-40229-1_4openalex-snapshot
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
inferred← citeshttps://doi.org/10.1007/978-3-319-61467-0_10openalex-snapshot
Testing a Saturation-Based Theorem Prover: Experiences and Challenges
inferred← citeshttps://doi.org/10.1007/978-3-319-63046-5_19openalex-snapshot
Detecting Inconsistencies in Large First-Order Knowledge Bases
inferred← citeshttps://doi.org/10.1007/978-3-319-91271-4_33openalex-snapshot
Teaching an Old Dog New Tricks
inferred← citeshttps://doi.org/10.1007/978-3-642-40537-2_14openalex-snapshot
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture
inferred← citeshttps://doi.org/10.1007/s00006-021-01164-1openalex-snapshot
Formalizing Geometric Algebra in Lean
inferred← citeshttps://doi.org/10.1007/s10817-015-9335-3openalex-snapshot
Semi-intelligible Isar Proofs from Machine-Generated Proofs
inferred← citeshttps://doi.org/10.1007/s10817-016-9362-8openalex-snapshot
A Learning-Based Fact Selector for Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/s10817-017-9404-xopenalex-snapshot
A Formally Verified Proof of the Central Limit Theorem
inferred← citeshttps://doi.org/10.1007/s10817-018-9481-5openalex-snapshot
A Formal Proof of the Expressiveness of Deep Learning
inferred← citeshttps://doi.org/10.1007/s10817-022-09629-zopenalex-snapshot
Theorem Proving as Constraint Solving with Coherent Logic
inferred← citeshttps://doi.org/10.1007/s10817-022-09643-1openalex-snapshot
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
inferred← citeshttps://doi.org/10.1007/s13218-024-00834-zopenalex-snapshot
Computer-Verified Foundations of Metaphysics
inferred← citeshttps://doi.org/10.1016/b978-0-444-51624-4.50004-6openalex-snapshot
History of Interactive Theorem Proving
inferred← citeshttps://doi.org/10.1016/j.jal.2012.12.002openalex-snapshot
LEO-II and Satallax on the Sledgehammer test bench
inferred← citeshttps://doi.org/10.1109/bigcom51056.2020.00018openalex-snapshot
Context-aware Generation of Proof Scripts for Theorem Proving
inferred← citeshttps://doi.org/10.1109/csf51468.2021.00006openalex-snapshot
Performing Security Proofs of Stateful Protocols
inferred← citeshttps://doi.org/10.1109/sp.2017.24openalex-snapshot
CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees
inferred← citeshttps://doi.org/10.1145/3158112openalex-snapshot
Safety and conservativity of definitions in HOL and Isabelle/HOL
inferred← citeshttps://doi.org/10.1145/3167094openalex-snapshot
Adapting proof automation to adapt proofs
inferred← citeshttps://doi.org/10.1145/3293880.3294087openalex-snapshot
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)
inferred← citeshttps://doi.org/10.1145/3437992.3439912openalex-snapshot
A modular Isabelle framework for verifying saturation provers
inferred← citeshttps://doi.org/10.14279/tuj.eceasst.72.1009openalex-snapshot
Conditional Lemma Discovery and Recursion Induction in Hipster
inferred← citeshttps://doi.org/10.15439/2018f106openalex-snapshot
Mizar Set Comprehension in Isabelle Framework
inferred← citeshttps://doi.org/10.15439/978-83-952357-0-2openalex-snapshot
Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems
inferred← citeshttps://doi.org/10.1561/2500000045openalex-snapshot
QED at Large: A Survey of Engineering of Formally Verified Software
inferred← citeshttps://doi.org/10.1609/aaai.v37i12.26759openalex-snapshot
Formally Verified Solution Methods for Markov Decision Processes
inferred← citeshttps://doi.org/10.17863/cam.23736openalex-snapshot
Computational logic: its origins and applications.
inferred← citeshttps://doi.org/10.21203/rs.3.rs-3598853/v1openalex-snapshot
Large Language Models' Understanding of Math: Source Criticism and Extrapolation
inferred← citeshttps://doi.org/10.29007/c25ropenalex-snapshot
Automated Theorem Proving for Prolog Verification
inferred← citeshttps://doi.org/10.29007/ddqmopenalex-snapshot
Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study
inferred← citeshttps://doi.org/10.29007/n6j7openalex-snapshot
Making Automatic Theorem Provers more Versatile
inferred← citeshttps://doi.org/10.29007/s6d1openalex-snapshot
Checkable Proofs for First-Order Theorem Proving
inferred← citeshttps://doi.org/10.29007/vrpkopenalex-snapshot
Extended Resolution as Certificates for Propositional Logic
inferred← citeshttps://doi.org/10.29007/zbdbopenalex-snapshot
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
inferred← citeshttps://doi.org/10.31219/osf.io/ac4spopenalex-snapshot
A Survey of Reasoning with Foundation Models
inferred← citeshttps://doi.org/10.4204/eptcs.187.2openalex-snapshot
Towards Enabling Overture as a Platform for Formal Notation IDEs
inferred← citeshttps://doi.org/10.4204/eptcs.210.6openalex-snapshot
Towards the Integration of an Intuitionistic First-Order Prover into Coq
inferred← citeshttps://doi.org/10.4204/eptcs.336openalex-snapshot
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving
inferred← citeshttps://doi.org/10.4204/eptcs.375.8openalex-snapshot
Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode
inferred← citeshttps://doi.org/10.48550/arxiv.1604.04639openalex-snapshot
ModelWizard: Toward Interactive Model Construction
inferred← citeshttps://doi.org/10.6092/issn.1972-5787/3690openalex-snapshot
Formal Verification of Language-Based Concurrent Noninterference
inferred← citeshttps://doi.org/10.7146/aul.118.106openalex-snapshot
On the Extensibility of Formal Methods Tools
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.