Buchumschlag

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Komel, Anja Petković, Rawson, Michael, Suda, Martin
Format:	Preprint
Veröffentlicht:	2025
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

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

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

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

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

act: Technical report
von: Paraskevopoulou, Zoe, et al.
Veröffentlicht: (2026)

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)

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

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

Wiring the Pi-calculus to Denotational Semantics
von: Sakayori, Ken, et al.
Veröffentlicht: (2026)

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
von: Pacheco, Leonardo
Veröffentlicht: (2026)

Satisfiability Modulo Theories for Verifying MILP Certificates
von: Wood, Kenan, et al.
Veröffentlicht: (2023)

Proof Nets for PiL (Full Version)
von: Acclavio, Matteo, et al.
Veröffentlicht: (2026)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
von: Feng, Nick, et al.
Veröffentlicht: (2024)

Proofs for Free in the $λΠ$-Calculus Modulo Theory
von: Traversié, Thomas
Veröffentlicht: (2024)

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

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
von: Afshari, Bahareh, et al.
Veröffentlicht: (2024)

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
von: Grabmayer, Clemens
Veröffentlicht: (2022)

Verified and Optimized Implementation of Orthologic Proof Search
von: Guilloud, Simon, et al.
Veröffentlicht: (2025)

Rewriting and Inductive Reasoning
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)

Efficient Neural Clause-Selection Reinforcement
von: Suda, Martin
Veröffentlicht: (2025)

Interpolation for the two-way modal mu-calculus
von: Kloibhofer, Johannes, et al.
Veröffentlicht: (2025)

Adding Negation to Lambda Mu
von: van Bakel, Steffen
Veröffentlicht: (2021)

Cut-elimination for the alternation-free modal mu-calculus
von: Afshari, Bahareh, et al.
Veröffentlicht: (2025)

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

Groups and Inverse Semigroups in Lambda Calculus
von: Bucciarelli, Antonio, et al.
Veröffentlicht: (2026)

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

Simplified and Verified: A Second Look at a Proof-Producing Union-Find Algorithm
von: Stevens, Lukas, et al.
Veröffentlicht: (2025)

A concrete model for a typed linear algebraic lambda calculus
von: Díaz-Caro, Alejandro, et al.
Veröffentlicht: (2018)

A Rewriting Theory for Quantum Lambda-Calculus
von: Faggian, Claudia, et al.
Veröffentlicht: (2024)

DRAFT: A Formally Verified Constructive Proof of the Consistency of Peano Arithmetic Using Ordinal Assignments
von: Bryce, Aaron, et al.
Veröffentlicht: (2026)

MCSAT Modulo Transcendental Arithmetics
von: Gallego-Hernández, Jorge, et al.
Veröffentlicht: (2026)

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

Congruence Closure Modulo Groups
von: Kim, Dohan
Veröffentlicht: (2023)

Variable Elimination as Rewriting in a Linear Lambda Calculus
von: Ehrhard, Thomas, et al.
Veröffentlicht: (2025)

The calculus of neo-Peircean relations
von: Bonchi, Filippo, et al.
Veröffentlicht: (2025)

Resource approximation for the $λμ$-calculus
von: Barbarossa, Davide
Veröffentlicht: (2024)

The higher dimensional propositional calculus
von: Bucciarelli, Antonio, et al.
Veröffentlicht: (2022)