Cover Image

Solving Set Constraints with Comprehensions and Bounded Quantifiers

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Mohamed, Mudathir, Feng, Nick, Reynolds, Andrew, Tinelli, Cesare, Barrett, Clark, Chechik, Marsha
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

Verifying SQL Queries using Theories of Tables and Relations
by: Mohamed, Mudathir, et al.
Published: (2024)

Generalized Optimization Modulo Theories
by: Tsiskaridze, Nestan, et al.
Published: (2024)

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

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

Applications of Quantified Constraint Solving over the Reals -- Bibliography
by: Ratschan, Stefan
Published: (2012)

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
by: Przybocki, Benjamin, et al.
Published: (2024)

$Π_{2}^{P}$ vs PSpace Dichotomy for the Quantified Constraint Satisfaction Problem
by: Zhuk, Dmitriy
Published: (2024)

Cubing for Tuning
by: Wu, Haoze, et al.
Published: (2025)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
by: Preiner, Mathias, et al.
Published: (2026)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
by: Cristiá, Maximiliano, et al.
Published: (2022)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
by: Pertseva, Elizaveta, et al.
Published: (2026)

Relational Hoare Logic for Realistically Modelled Machine Code
by: Mazzucato, Denis, et al.
Published: (2025)

Identifying Tractable Quantified Temporal Constraints within Ord-Horn
by: Rydval, Jakub, et al.
Published: (2024)

Can LLM Aid in Solving Constraints with Inductive Definitions?
by: Feng, Weizhi, et al.
Published: (2026)

Certified Branch-and-Bound MaxSAT Solving (Extended Version)
by: Vandesande, Dieter, et al.
Published: (2025)

Solving SAT By Computing A Stable Set Of Points In Clusters
by: Goldberg, Eugene
Published: (2025)

Bounded Structural Model Finding with Symbolic Data Constraints
by: Boronat, Artur
Published: (2026)

Learning Branching-Time Properties in CTL and ATL via Constraint Solving
by: Bordais, Benjamin, et al.
Published: (2024)

Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
by: Cristiá, Maximiliano, et al.
Published: (2025)

The termination of Nielsen transformations applied to word equations with length constraints
by: Przybocki, Benjamin, et al.
Published: (2025)

Embedded Finite Models Beyond Restricted Quantifier Collapse
by: Benedikt, Michael, et al.
Published: (2023)

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

A Coalgebraic Semantics for Intuitionistic Modal Logic
by: Almeida, Rodrigo Nicolau, et al.
Published: (2024)

Complexity of Weighted First-Order Model Counting in the Two-Variable Fragment with Counting Quantifiers: A Bound to Beat
by: Tóth, Jan, et al.
Published: (2024)

Dependence Logics in Temporal Settings
by: Baltag, Alexandru, et al.
Published: (2022)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
by: Lyon, Tim S., et al.
Published: (2026)

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

On proving consistency of equational theories in Bounded Arithmetic
by: Beckmann, Arnold, et al.
Published: (2022)

Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
by: Tiurin, Aleksei, et al.
Published: (2024)

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

DateSAT: A Framework for Solving Date and Period Constraints
by: Cui, Leyi, et al.
Published: (2026)

Towards Constraint Temporal Answer Set Programming
by: Cabalar, Pedro, et al.
Published: (2025)

Solving Decision Theory Problems with Probabilistic Answer Set Programming
by: Azzolini, Damiano, et al.
Published: (2024)

Three Fundamental Questions in Modern Infinite-Domain Constraint Satisfaction
by: Pinsker, Michael, et al.
Published: (2025)

From Quantifier Depth to Quantifier Number: Separating Structures with k Variables
by: Vinall-Smeeth, Harry
Published: (2023)

Extracting Policies from Quantified Answer Set Programs
by: Diéguez, Martín, et al.
Published: (2026)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

Modal Fragments
by: Bezhanishvili, Nick, et al.
Published: (2026)