Cover Image

Experimental Results for Vampire on the Equational Theories Project

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Janota, Mikoláš
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Case Study: Saturations as Explicit Models in Equational Theories
by: Janota, Mikoláš, et al.
Published: (2026)

First Experiments with Neural cvc5
by: Piepenbrock, Jelle, et al.
Published: (2025)

Breaking Symmetries with Involutions
by: Codish, Michael, et al.
Published: (2025)

Breaking Symmetries from a Set-Covering Perspective
by: Codish, Michael, et al.
Published: (2025)

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

Quantifier Instantiations: To Mimic or To Revolt?
by: Jakubův, Jan, et al.
Published: (2025)

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

From MBQI to Enumerative Instantiation and Back
by: Dančo, Marek, et al.
Published: (2025)

Cube-based Isomorph-free Finite Model Finding
by: Chow, Choiwah, et al.
Published: (2025)

Symbolic Computation for All the Fun
by: Brown, Chad E., et al.
Published: (2024)

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

Breaking Symmetries in Quantified Graph Search: A Comparative Study
by: Janota, Mikoláš, et al.
Published: (2025)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
by: Ratschan, Stefan, et al.
Published: (2026)

Reintroducing the Second Player in EPR
by: Chew, Leroy, et al.
Published: (2026)

Complete Symmetry Breaking for Finite Models
by: Dančo, Marek, et al.
Published: (2025)

CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases
by: Orvalho, Pedro, et al.
Published: (2024)

SAT-Based Techniques for Lexicographically Smallest Finite Models
by: Janota, Mikoláš, et al.
Published: (2025)

Solving Hard Mizar Problems with Instantiation and Strategy Invention
by: Jakubův, Jan, et al.
Published: (2024)

Machine Learning for Quantifier Selection in cvc5
by: Jakubův, Jan, et al.
Published: (2024)

The Vampire Diary
by: Bártek, Filip, et al.
Published: (2025)

Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits
by: Orvalho, Pedro, et al.
Published: (2025)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)

When Agda met Vampire
by: Šinkarovs, Artjoms, et al.
Published: (2026)

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
by: Baader, Franz, et al.
Published: (2026)

Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
by: Komel, Anja Petković, et al.
Published: (2025)

Non-Derivability Results in Polymorphic Dependent Type Theory
by: Geuvers, Herman
Published: (2026)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
by: Jeanteur, Simon, et al.
Published: (2023)

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
by: Bolan, Matthew, et al.
Published: (2025)

Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
by: Nantes-Sobrinho, Daniele, et al.
Published: (2025)

A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
by: Bergstra, Jan A, et al.
Published: (2023)

Deciding Equations in the Time Warp Algebra
by: van Gool, Sam, et al.
Published: (2023)

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
by: Nakamura, Yoshiki
Published: (2025)

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
by: Aoto, Takahito, et al.
Published: (2024)

A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory
by: Affeldt, Reynald, et al.
Published: (2023)

Some General Completeness Results for Propositionally Quantified Modal Logics
by: Ding, Yifeng, et al.
Published: (2024)

On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
by: Lyon, Tim S.
Published: (2024)

Rings and Boolean Algebras as Algebraic Theories
by: De Faveri, Arturo
Published: (2025)

Primitive Recursive Dependent Type Theory
by: Buchholtz, Ulrik, et al.
Published: (2024)

Fixed Point Theorems in Computability Theory
by: Terwijn, Sebastiaan A.
Published: (2024)

Characterizing Sets of Theories That Can Be Disjointly Combined
by: Przybocki, Benjamin, et al.
Published: (2025)