Buchumschlag

Case Study: Saturations as Explicit Models in Equational Theories

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Janota, Mikoláš, Rawson, Michael, Schulz, Stephan
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

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

Breaking Symmetries with Involutions
von: Codish, Michael, et al.
Veröffentlicht: (2025)

Breaking Symmetries from a Set-Covering Perspective
von: Codish, Michael, et al.
Veröffentlicht: (2025)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
von: Janota, Mikoláš, et al.
Veröffentlicht: (2026)

Towards Learning Infinite SMT Models (Work in Progress)
von: Janota, Mikoláš, et al.
Veröffentlicht: (2025)

Cube-based Isomorph-free Finite Model Finding
von: Chow, Choiwah, et al.
Veröffentlicht: (2025)

Quantifier Instantiations: To Mimic or To Revolt?
von: Jakubův, Jan, et al.
Veröffentlicht: (2025)

From MBQI to Enumerative Instantiation and Back
von: Dančo, Marek, et al.
Veröffentlicht: (2025)

First Experiments with Neural cvc5
von: Piepenbrock, Jelle, et al.
Veröffentlicht: (2025)

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

Breaking Symmetries in Quantified Graph Search: A Comparative Study
von: Janota, Mikoláš, et al.
Veröffentlicht: (2025)

Complete Symmetry Breaking for Finite Models
von: Dančo, Marek, et al.
Veröffentlicht: (2025)

Symbolic Computation for All the Fun
von: Brown, Chad E., et al.
Veröffentlicht: (2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
von: Brown, Chad E., et al.
Veröffentlicht: (2025)

SAT-Based Techniques for Lexicographically Smallest Finite Models
von: Janota, Mikoláš, et al.
Veröffentlicht: (2025)

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
von: Ratschan, Stefan, et al.
Veröffentlicht: (2026)

Reintroducing the Second Player in EPR
von: Chew, Leroy, et al.
Veröffentlicht: (2026)

Solving Hard Mizar Problems with Instantiation and Strategy Invention
von: Jakubův, Jan, et al.
Veröffentlicht: (2024)

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

Machine Learning for Quantifier Selection in cvc5
von: Jakubův, Jan, et al.
Veröffentlicht: (2024)

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

On Explicit Solutions to Fixed-Point Equations in Propositional Dynamic Logic
von: Lyon, Tim S.
Veröffentlicht: (2024)

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

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

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

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

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

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

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
von: Bezem, Marc, et al.
Veröffentlicht: (2026)

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

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

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

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

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

Program Synthesis in Saturation
von: Hozzová, Petra, et al.
Veröffentlicht: (2024)

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

Lemmas: Generation, Selection, Application
von: Rawson, Michael, et al.
Veröffentlicht: (2023)

The Pebble-Relation Comonad in Finite Model Theory
von: Montacute, Yoàv, et al.
Veröffentlicht: (2021)

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

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