Imagen de Portada

Towards Learning Infinite SMT Models (Work in Progress)

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Janota, Mikoláš, Piotrowski, Bartosz, Chvalovský, Karel
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

Experimental Results for Vampire on the Equational Theories Project
por: Janota, Mikoláš
Publicado: (2025)

Breaking Symmetries with Involutions
por: Codish, Michael, et al.
Publicado: (2025)

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

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

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

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

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

First Experiments with Neural cvc5
por: Piepenbrock, Jelle, et al.
Publicado: (2025)

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

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

Regularization in Spider-Style Strategy Discovery and Schedule Construction
por: Bártek, Filip, et al.
Publicado: (2024)

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

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

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

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

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

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

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

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

Towards SMT Solver Stability via Input Normalization
por: Amrollahi, Daneshvar, et al.
Publicado: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
por: Mohamed, Abdalrhman, et al.
Publicado: (2025)

Efficient Volume Computation for SMT Formulas
por: Shaw, Arijit, et al.
Publicado: (2025)

An SMT Theory for n-Indexed Sequences
por: Hara, Hichem Rami Ait El, et al.
Publicado: (2024)

An SMT-LIB Theory of Finite Fields
por: Hader, Thomas, et al.
Publicado: (2024)

Hint-Based SMT Proof Reconstruction
por: Clune, Joshua, et al.
Publicado: (2026)

On SMT Theory Design: The Case of Sequences
por: Hara, Hichem Rami Ait El, et al.
Publicado: (2024)

Number theory combination: natural density and SMT
por: Toledo, Guilherme V., et al.
Publicado: (2025)

Integer Reasoning Modulo Different Constants in SMT
por: Pertseva, Elizaveta, et al.
Publicado: (2025)

Invariant Checking for SMT-based Systems with Quantifiers
por: Redondi, Gianluca, et al.
Publicado: (2024)

System ASPMT2SMT:Computing ASPMT Theories by SMT Solvers
por: Bartholomew, Michael, et al.
Publicado: (2025)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
por: Huvar, Ondřej, et al.
Publicado: (2026)

Infinite trees
por: Goy, Alexandre
Publicado: (2025)

Towards Automatic Linearization via SMT Solving
por: Cao, Jian, et al.
Publicado: (2024)

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

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

A Relational Theory of Grounding and a new Grounder for SMT
por: Carbonnelle, Pierre
Publicado: (2026)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
por: Hader, Thomas, et al.
Publicado: (2024)

SMT(LIA) Sampling with High Diversity
por: Lai, Yong, et al.
Publicado: (2025)