Cover Image

From MBQI to Enumerative Instantiation and Back

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Dančo, Marek, Hozzová, Petra, 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

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

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

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

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

Experimental Results for Vampire on the Equational Theories Project
by: Janota, Mikoláš
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)

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

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

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

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

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
by: Hozzová, Petra, et al.
Published: (2025)

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

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

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

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)

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

Program Synthesis in Saturation
by: Hozzová, Petra, et al.
Published: (2024)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
by: Hozzová, Petra, et al.
Published: (2024)

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

Completeness of Synthesis under Realizability Assumptions using Superposition
by: Hajdu, Márton, et al.
Published: (2026)

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

Getting Saturated with Induction
by: Hajdu, Márton, et al.
Published: (2024)

Synthesis Benchmarks for Automated Reasoning
by: Hajdu, Márton, et al.
Published: (2025)

Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL
by: Bartl, Lukas, et al.
Published: (2025)

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)

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
by: Ge, Rui, et al.
Published: (2024)

Enumerating Independent Linear Inferences
by: Das, Anupam, et al.
Published: (2021)

On Enumerating Short Projected Models
by: Möhle, Sibylle, et al.
Published: (2021)

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

Disjoint Partial Enumeration without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2023)

Extending CDCL-based Model Enumeration with Weights
by: Spallitta, Giuseppe, et al.
Published: (2026)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
by: Spallitta, Giuseppe, et al.
Published: (2024)

FO-Query Enumeration over SLP-Compressed Structures of Bounded Degree
by: Lohrey, Markus, et al.
Published: (2025)

A Simple and Effective ASP-Based Tool for Enumerating Minimal Hitting Sets
by: Kabir, Mohimenul, et al.
Published: (2025)

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
by: Civini, Emanuele, et al.
Published: (2026)

Enumerating Minimal Unsatisfiable Cores of LTLf formulas
by: Ielo, Antonio, et al.
Published: (2024)

Using Color Refinement to Boost Enumeration and Counting for Acyclic CQs of Binary Schemas
by: Riveros, Cristian, et al.
Published: (2024)