Buchumschlag

Automating Bitvector and Finite Field Equivalence Proofs in Lean

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Pertseva, Elizaveta, Robert, Valentin, Barrett, Clark, Parker, James
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Integer Reasoning Modulo Different Constants in SMT
von: Pertseva, Elizaveta, et al.
Veröffentlicht: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
von: Qian, Yicheng, et al.
Veröffentlicht: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
von: Mohamed, Abdalrhman, et al.
Veröffentlicht: (2025)

Lean on Vampire Proofs (Short Paper)
von: Bodingbauer, Jonas, et al.
Veröffentlicht: (2026)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
von: Aniva, Leni, et al.
Veröffentlicht: (2026)

Proof Minimization in Neural Network Verification
von: Isac, Omri, et al.
Veröffentlicht: (2025)

CSLib: The Lean Computer Science Library
von: Barrett, Clark, et al.
Veröffentlicht: (2026)

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
von: Przybocki, Benjamin, et al.
Veröffentlicht: (2024)

PICID: Proof-Driven Clause Learning in Neural Network Verification
von: Isac, Omri, et al.
Veröffentlicht: (2025)

LeanArchitect: Automating Blueprint Generation for Humans and AI
von: Zhu, Thomas, et al.
Veröffentlicht: (2026)

PBLean: Pseudo-Boolean Proof Certificates for Lean 4
von: Szeider, Stefan
Veröffentlicht: (2026)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
von: Preiner, Mathias, et al.
Veröffentlicht: (2026)

Generalized Optimization Modulo Theories
von: Tsiskaridze, Nestan, et al.
Veröffentlicht: (2024)

Cubing for Tuning
von: Wu, Haoze, et al.
Veröffentlicht: (2025)

Proofs that Modify Proofs, 1/2
von: Towsner, Henry
Veröffentlicht: (2025)

Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
von: Yin, David, et al.
Veröffentlicht: (2025)

Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
von: Cesco, Arnaldo, et al.
Veröffentlicht: (2021)

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
von: Kolesar, John, et al.
Veröffentlicht: (2025)

Automated Tactics for Polynomial Reasoning in Lean 4
von: Shen, Hao, et al.
Veröffentlicht: (2026)

Towards Language Model Guided TLA+ Proof Automation
von: Zhou, Yuhao, et al.
Veröffentlicht: (2025)

Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
von: Shen, Austin, et al.
Veröffentlicht: (2026)

Verifying SQL Queries using Theories of Tables and Relations
von: Mohamed, Mudathir, et al.
Veröffentlicht: (2024)

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
von: Tiurin, Aleksei, et al.
Veröffentlicht: (2024)

The Proof Analysis Problem
von: Arteche, Noel, et al.
Veröffentlicht: (2025)

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
von: Ospanov, Azim, et al.
Veröffentlicht: (2025)

An SMT-LIB Theory of Finite Fields
von: Hader, Thomas, et al.
Veröffentlicht: (2024)

Kimina Lean Server: A High-Performance Lean Server for Large-Scale Verification
von: Santos, Marco Dos, et al.
Veröffentlicht: (2025)

Proof-theoretic Semantics for Second-order Logic
von: Gheorghiu, Alexander V., et al.
Veröffentlicht: (2025)

Proof-theoretic Semantics for the Logic of Bunched Implications
von: Gu, Tao, et al.
Veröffentlicht: (2023)

Proof-theoretic Semantics for First-order Logic
von: Gheorghiu, Alexander V.
Veröffentlicht: (2024)

Cyclic Proofs for iGL via Corecursion
von: Miranda, Borja Sierra
Veröffentlicht: (2023)

Proof Complexity of Linear Logics
von: Tabatabai, Amirhossein Akbar, et al.
Veröffentlicht: (2026)

Intuitionistic Propositional Logic in Lean
von: Trufaş, Dafina
Veröffentlicht: (2024)

LeanTutor: Towards a Verified AI Mathematical Proof Tutor
von: Patel, Manooshree, et al.
Veröffentlicht: (2025)

Proof-Theoretic Functional Completeness for the Connexive Logic C
von: Ayhan, Sara, et al.
Veröffentlicht: (2025)

Proof Theory and Decision Procedures for Deontic STIT Logics
von: Lyon, Tim S., et al.
Veröffentlicht: (2024)

Universal Proof Theory, TACL 2022 Lecture Notes
von: Iemhoff, Rosalie, et al.
Veröffentlicht: (2023)

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
von: Aniva, Leni, et al.
Veröffentlicht: (2024)

Proof complexity of positive branching programs
von: Das, Anupam, et al.
Veröffentlicht: (2021)

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
von: Kasaura, Kazumi, et al.
Veröffentlicht: (2025)