Cover Image

Program Synthesis in Saturation

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Hozzová, Petra, Kovács, Laura, Norman, Chase, Voronkov, Andrei
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Partial Redundancy in Saturation
by: Hajdu, Márton, et al.
Published: (2025)

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

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

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

Term Ordering Diagrams
by: Hajdu, Márton, et al.
Published: (2025)

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

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

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

Saturating Sorting without Sorts
by: Georgiou, Pamina, et al.
Published: (2024)

Positive Almost-Sure Termination of Polynomial Random Walks
by: Winkler, Lorenz, et al.
Published: (2025)

Linear Loop Synthesis for Quadratic Invariants
by: Hitarth, S., et al.
Published: (2023)

Rewriting and Inductive Reasoning
by: Hajdu, Márton, et al.
Published: (2024)

Spanning Matrices via Satisfiability Solving
by: Eisenhofer, Clemens, et al.
Published: (2024)

Lazy Reimplication in Chronological Backtracking
by: Coutelier, Robin, et al.
Published: (2025)

Finding Connections via Satisfiability Solving
by: Eisenhofer, Clemens, et al.
Published: (2026)

Constraint Learning for Non-confluent Proof Search
by: Rawson, Michael, et al.
Published: (2026)

Canonical for Automated Theorem Proving in Lean
by: Norman, Chase, et al.
Published: (2025)

Implementing Dependent Type Theory Inhabitation and Unification
by: Norman, Chase, et al.
Published: (2026)

Certificate-Aware Property-Directed Reachability
by: Ferdowsi, Arman, et al.
Published: (2026)

SAT-Based Subsumption Resolution
by: Coutelier, Robin, et al.
Published: (2024)

On Solving String Equations via Powers and Parikh Images
by: Eisenhofer, Clemens, et al.
Published: (2026)

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

SAT Solving for Variants of First-Order Subsumption
by: Coutelier, Robin, et al.
Published: (2024)

PolySAT: Word-level Bit-vector Reasoning in Z3
by: Rath, Jakob, et al.
Published: (2024)

Lean on Vampire Proofs (Short Paper)
by: Bodingbauer, Jonas, et al.
Published: (2026)

Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations
by: Nakamura, Yoshiki
Published: (2023)

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

An Expressive Coalgebraic Modal Logic for Cellular Automata
by: Basold, Henning, et al.
Published: (2025)

Local structure of idempotent algebras I
by: Bulatov, Andrei A.
Published: (2020)

Recursive Program Synthesis from Sketches and Mixed-Quantifier Properties
by: Egolf, Derek, et al.
Published: (2026)

Consistent Update Synthesis via Privatized Beliefs
by: Schlögl, Thomas, et al.
Published: (2024)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
by: Jeanteur, Simon, et al.
Published: (2023)

Programs as Singularities
by: Murfet, Daniel, et al.
Published: (2025)

Realizing the totally unordered structure of ordinals
by: Fontanella, Laura, et al.
Published: (2025)

Graded Monads and Behavioural Equivalence Games
by: Ford, Chase, et al.
Published: (2022)

Probabilistic Model Checking: Applications and Trends
by: Kwiatkowska, Marta, et al.
Published: (2025)

Scaling CheckMate for Game-Theoretic Security
by: Rain, Sophie, et al.
Published: (2024)

LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
by: King, Daragh, et al.
Published: (2025)

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
by: King, Daragh, et al.
Published: (2025)