Cover Image

Hint-Based SMT Proof Reconstruction

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Clune, Joshua, Barbosa, Haniel, Avigad, Jeremy
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications
by: Barbosa, Haniel, et al.
Published: (2025)

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
by: Ahuja, Riyaz, et al.
Published: (2026)

A Proof-Producing Compiler for Blockchain Applications
by: Avigad, Jeremy, et al.
Published: (2025)

LeanArchitect: Automating Blueprint Generation for Humans and AI
by: Zhu, Thomas, et al.
Published: (2026)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
by: Rowney, Tate, et al.
Published: (2026)

Implementing Dependent Type Theory Inhabitation and Unification
by: Norman, Chase, et al.
Published: (2026)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
by: Janota, Mikoláš, et al.
Published: (2026)

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
by: Hozzová, Petra, et al.
Published: (2025)

Efficient Volume Computation for SMT Formulas
by: Shaw, Arijit, et al.
Published: (2025)

An SMT Theory for n-Indexed Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

An SMT-LIB Theory of Finite Fields
by: Hader, Thomas, et al.
Published: (2024)

On SMT Theory Design: The Case of Sequences
by: Hara, Hichem Rami Ait El, et al.
Published: (2024)

Number theory combination: natural density and SMT
by: Toledo, Guilherme V., et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

Invariant Checking for SMT-based Systems with Quantifiers
by: Redondi, Gianluca, et al.
Published: (2024)

System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
by: Bartholomew, Michael, et al.
Published: (2025)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
by: Huvar, Ondřej, et al.
Published: (2026)

Towards Learning Infinite SMT Models (Work in Progress)
by: Janota, Mikoláš, et al.
Published: (2025)

Towards SMT Solver Stability via Input Normalization
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Certified Knowledge Compilation with Application to Formally Verified Model Counting
by: Bryant, Randal E., et al.
Published: (2025)

Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols
by: Sojakova, Kristina, et al.
Published: (2025)

Proofs that Modify Proofs, 1/2
by: Towsner, Henry
Published: (2025)

A Relational Theory of Grounding and a new Grounder for SMT
by: Carbonnelle, Pierre
Published: (2026)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs
by: Hassnain, Muhammad, et al.
Published: (2025)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
by: Hader, Thomas, et al.
Published: (2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
by: Brown, Chad E., et al.
Published: (2025)

SMT(LIA) Sampling with High Diversity
by: Lai, Yong, et al.
Published: (2025)

An Encoding for CLP Problems in SMT-LIB
by: Amrollahi, Daneshvar, et al.
Published: (2024)

Automated Process Planning Based on a Semantic Capability Model and SMT
by: Köcher, Aljosha, et al.
Published: (2023)

A Local Search Algorithm for MaxSMT(LIA)
by: He, Xiang, et al.
Published: (2024)

SMT-Layout: A MaxSMT-based Approach Supporting Real-time Interaction of Real-world GUI Layout
by: Li, Bohan, et al.
Published: (2024)

From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
by: Gheorghiu, Alexander V., et al.
Published: (2022)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
by: Civini, Emanuele, et al.
Published: (2026)

Approximate SMT Counting Beyond Discrete Domains
by: Shaw, Arijit, et al.
Published: (2025)