Image de couverture de livre

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Ratschan, Stefan, Nugraha, Anggha, Janota, Mikoláš, Dančo, Marek
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

From MBQI to Enumerative Instantiation and Back
par: Dančo, Marek, et autres
Publié: (2025)

Complete Symmetry Breaking for Finite Models
par: Dančo, Marek, et autres
Publié: (2025)

Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem
par: Lipparini, Enrico, et autres
Publié: (2023)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO
par: Brown, Chad E., et autres
Publié: (2025)

Quantifier Instantiations: To Mimic or To Revolt?
par: Jakubův, Jan, et autres
Publié: (2025)

Experimental Results for Vampire on the Equational Theories Project
par: Janota, Mikoláš
Publié: (2025)

Breaking Symmetries in Quantified Graph Search: A Comparative Study
par: Janota, Mikoláš, et autres
Publié: (2025)

Symbolic Computation for All the Fun
par: Brown, Chad E., et autres
Publié: (2024)

Applications of Quantified Constraint Solving over the Reals -- Bibliography
par: Ratschan, Stefan
Publié: (2012)

LLM2SMT: Building an SMT Solver with Zero Human-Written Code
par: Janota, Mikoláš, et autres
Publié: (2026)

Breaking Symmetries with Involutions
par: Codish, Michael, et autres
Publié: (2025)

Breaking Symmetries from a Set-Covering Perspective
par: Codish, Michael, et autres
Publié: (2025)

Deciding Predicate Logical Theories of Real-Valued Functions
par: Ratschan, Stefan
Publié: (2023)

Case Study: Saturations as Explicit Models in Equational Theories
par: Janota, Mikoláš, et autres
Publié: (2026)

Towards Learning Infinite SMT Models (Work in Progress)
par: Janota, Mikoláš, et autres
Publié: (2025)

First Experiments with Neural cvc5
par: Piepenbrock, Jelle, et autres
Publié: (2025)

Cube-based Isomorph-free Finite Model Finding
par: Chow, Choiwah, et autres
Publié: (2025)

Machine Learning for Quantifier Selection in cvc5
par: Jakubův, Jan, et autres
Publié: (2024)

Reintroducing the Second Player in EPR
par: Chew, Leroy, et autres
Publié: (2026)

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology
par: Huvar, Ondřej, et autres
Publié: (2026)

CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases
par: Orvalho, Pedro, et autres
Publié: (2024)

Efficient Solving of Quantified Inequality Constraints over the Real Numbers
par: Ratschan, Stefan
Publié: (2002)

SAT-Based Techniques for Lexicographically Smallest Finite Models
par: Janota, Mikoláš, et autres
Publié: (2025)

Solving Hard Mizar Problems with Instantiation and Strategy Invention
par: Jakubův, Jan, et autres
Publié: (2024)

Satisfiability Modulo Theories for Verifying MILP Certificates
par: Wood, Kenan, et autres
Publié: (2023)

Satisfiability of Quantified Boolean Announcements
par: van Ditmarsch, Hans, et autres
Publié: (2022)

Input-based Three-valued Abstraction Refinement
par: Onderka, Jan, et autres
Publié: (2024)

Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits
par: Orvalho, Pedro, et autres
Publié: (2025)

Partial Quantifier Elimination By Certificate Clauses
par: Goldberg, Eugene
Publié: (2020)

parSAT: Parallel Solving of Floating-Point Satisfiability
par: Krahl, Markus, et autres
Publié: (2025)

Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
par: Chatterjee, Krishnendu, et autres
Publié: (2024)

Neuro-Symbolic Constrained Optimization for Cloud Application Deployment via Graph Neural Networks and Satisfiability Modulo Theory
par: Erascu, Madalina
Publié: (2025)

Formalising Inductive and Coinductive Containers
par: Damato, Stefania, et autres
Publié: (2024)

iSMC: A BDD-based Symbolic Model Checker with Interactive Certification
par: Czerner, Philipp, et autres
Publié: (2026)

Hyperproperty Verification as CHC Satisfiability
par: Itzhaky, Shachar, et autres
Publié: (2023)

Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees
par: Li, Jinzhao, et autres
Publié: (2023)

Finding Connections via Satisfiability Solving
par: Eisenhofer, Clemens, et autres
Publié: (2026)

Satisfiability Modulo Exponential Integer Arithmetic
par: Frohn, Florian, et autres
Publié: (2024)

Spanning Matrices via Satisfiability Solving
par: Eisenhofer, Clemens, et autres
Publié: (2024)

Satisfiability in Łukasiewicz logic and its unbounded relative
par: Haniková, Zuzana, et autres
Publié: (2025)