Buchumschlag

Lean on Vampire Proofs (Short Paper)

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Bodingbauer, Jonas, Hajdu, Márton, Kovács, Laura, Polaczek, Axel, Rawson, Michael
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

Rewriting and Inductive Reasoning
von: Hajdu, Márton, et al.
Veröffentlicht: (2024)

The Vampire Diary
von: Bártek, Filip, et al.
Veröffentlicht: (2025)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
von: Komel, Anja Petković, et al.
Veröffentlicht: (2025)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
von: Jeanteur, Simon, et al.
Veröffentlicht: (2023)

Constraint Learning for Non-confluent Proof Search
von: Rawson, Michael, et al.
Veröffentlicht: (2026)

Partial Redundancy in Saturation
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

When Agda met Vampire
von: Šinkarovs, Artjoms, et al.
Veröffentlicht: (2026)

Saturating Sorting without Sorts
von: Georgiou, Pamina, et al.
Veröffentlicht: (2024)

Term Ordering Diagrams
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

Completeness of Synthesis under Realizability Assumptions using Superposition
von: Hajdu, Márton, et al.
Veröffentlicht: (2026)

Getting Saturated with Induction
von: Hajdu, Márton, et al.
Veröffentlicht: (2024)

Finding Connections via Satisfiability Solving
von: Eisenhofer, Clemens, et al.
Veröffentlicht: (2026)

Spanning Matrices via Satisfiability Solving
von: Eisenhofer, Clemens, et al.
Veröffentlicht: (2024)

SAT-Based Subsumption Resolution
von: Coutelier, Robin, et al.
Veröffentlicht: (2024)

Synthesis Benchmarks for Automated Reasoning
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

SAT Solving for Variants of First-Order Subsumption
von: Coutelier, Robin, et al.
Veröffentlicht: (2024)

A Higher-Order Vampire (Short Paper)
von: Bhayat, Ahmed, et al.
Veröffentlicht: (2024)

Scaling CheckMate for Game-Theoretic Security
von: Rain, Sophie, et al.
Veröffentlicht: (2024)

Experimental Results for Vampire on the Equational Theories Project
von: Janota, Mikoláš
Veröffentlicht: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
von: Pertseva, Elizaveta, et al.
Veröffentlicht: (2026)

Case Study: Saturations as Explicit Models in Equational Theories
von: Janota, Mikoláš, et al.
Veröffentlicht: (2026)

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

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)

Positive Almost-Sure Termination of Polynomial Random Walks
von: Winkler, Lorenz, 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)

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

Superposition with Delayed Unification
von: Bhayat, Ahmed, et al.
Veröffentlicht: (2024)

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

Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds
von: Li, Jiawei, et al.
Veröffentlicht: (2024)

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

Lazy Reimplication in Chronological Backtracking
von: Coutelier, Robin, et al.
Veröffentlicht: (2025)

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)