On the public citation graph

Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs

https://doi.org/10.29007/zbdb
0 signed · 35 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.
Claim with ORCID
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.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

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-1-4684-2001-2_9openalex-snapshot
Reducibility among Combinatorial Problems
inferredcites →https://doi.org/10.1007/978-3-540-25984-8_15openalex-snapshot
System Description: E 0.81
inferredcites →https://doi.org/10.1007/978-3-540-68279-0_8openalex-snapshot
Reducibility Among Combinatorial Problems
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-14052-5_14openalex-snapshot
Fast LCF-Style Proof Reconstruction for Z3
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-31365-3_11openalex-snapshot
Satallax: An Automatic Higher-Order Prover
inferredcites →https://doi.org/10.1007/978-3-642-36742-7_34openalex-snapshot
Encoding Monomorphic and Polymorphic Types
inferredcites →https://doi.org/10.1007/978-3-642-38574-2_18openalex-snapshot
PRocH: Proof Reconstruction for HOL Light
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.1007/s10817-009-9143-8openalex-snapshot
The TPTP Problem Library and Associated Infrastructure
inferredcites →https://doi.org/10.1007/s10817-012-9267-0openalex-snapshot
Methods of Lemma Extraction in Natural Deduction Proofs
inferredcites →https://doi.org/10.1016/j.ic.2004.10.011openalex-snapshot
Translation of resolution proofs into short first-order proofs without choice axioms
inferredcites →https://doi.org/10.1016/j.jal.2012.12.002openalex-snapshot
LEO-II and Satallax on the Sledgehammer test bench
inferredcites →https://doi.org/10.1023/a:1005872405899openalex-snapshot
WALDMEISTER - High-Performance Equational Deduction
inferredcites →https://doi.org/10.2307/2266170openalex-snapshot
A formulation of the simple theory of types
inferredcites →https://doi.org/10.29007/36dtopenalex-snapshot
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers
inferredcites →https://doi.org/10.29007/s1tsopenalex-snapshot
Escape to Mizar from ATPs
inferredcites →https://doi.org/10.29007/tnfdopenalex-snapshot
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers
inferredcites →https://doi.org/10.29007/wm8bopenalex-snapshot
Redirecting Proofs by Contradiction

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-319-08434-3_27openalex-snapshot
Automated Improving of Proof Legibility in the Mizar System
inferred← citeshttps://doi.org/10.1007/978-3-319-08434-3_28openalex-snapshot
A Vernacular for Coherent Logic
inferred← citeshttps://doi.org/10.1007/978-3-319-24246-0_21openalex-snapshot
Lemmatization for Stronger Reasoning in Large Theories
inferred← citeshttps://doi.org/10.1007/s10817-015-9330-8openalex-snapshot
MizAR 40 for Mizar 40
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-022-09643-1openalex-snapshot
Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
inferred← citeshttps://doi.org/10.1016/j.jsc.2014.09.032openalex-snapshot
Learning-assisted theorem proving with millions of lemmas
inferred← citeshttps://doi.org/10.1145/3703595.3705877openalex-snapshot
Tactic Script Optimisation for Aesop
inferred← citeshttps://doi.org/10.1515/9783111386690-009openalex-snapshot
1857 Automatische Inferenz
inferred← citeshttps://doi.org/10.2168/lmcs-10(3:23)2014openalex-snapshot
Improving legibility of natural deduction proofs is not trivial
inferred← citeshttps://doi.org/10.29007/5b7wopenalex-snapshot
My Life with an Automatic Theorem Prover
inferred← citeshttps://doi.org/10.29007/wm8bopenalex-snapshot
Redirecting Proofs by Contradiction
inferred← citeshttps://doi.org/10.6092/issn.1972-5787/4593openalex-snapshot
Hammering towards QED
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.