Buchumschlag

Completeness of Synthesis under Realizability Assumptions using Superposition

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Hajdu, Márton, Hozzová, Petra, Kovács, Laura, Wagner, Eva Maria
Format:	Preprint
Veröffentlicht:	2026
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Synthesis Benchmarks for Automated Reasoning
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

Getting Saturated with Induction
von: Hajdu, Márton, et al.
Veröffentlicht: (2024)

Program Synthesis in Saturation
von: Hozzová, Petra, et al.
Veröffentlicht: (2024)

Rewriting and Inductive Reasoning
von: Hajdu, Márton, et al.
Veröffentlicht: (2024)

Partial Redundancy in Saturation
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

Saturating Sorting without Sorts
von: Georgiou, Pamina, et al.
Veröffentlicht: (2024)

Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
von: Hozzová, Petra, et al.
Veröffentlicht: (2025)

Term Ordering Diagrams
von: Hajdu, Márton, et al.
Veröffentlicht: (2025)

Lean on Vampire Proofs (Short Paper)
von: Bodingbauer, Jonas, et al.
Veröffentlicht: (2026)

The Vampire Diary
von: Bártek, Filip, et al.
Veröffentlicht: (2025)

From MBQI to Enumerative Instantiation and Back
von: Dančo, Marek, et al.
Veröffentlicht: (2025)

Overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification
von: Hozzová, Petra, et al.
Veröffentlicht: (2024)

Realizing the totally unordered structure of ordinals
von: Fontanella, Laura, et al.
Veröffentlicht: (2025)

On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
von: Waldmann, Uwe
Veröffentlicht: (2024)

CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
von: Jeanteur, Simon, et al.
Veröffentlicht: (2023)

Positive Almost-Sure Termination of Polynomial Random Walks
von: Winkler, Lorenz, et al.
Veröffentlicht: (2025)

Linear Loop Synthesis for Quadratic Invariants
von: Hitarth, S., et al.
Veröffentlicht: (2023)

The Arithmetical Hierarchy: A Realizability-Theoretic Perspective
von: Kihara, Takayuki
Veröffentlicht: (2024)

Superposition with Delayed Unification
von: Bhayat, Ahmed, et al.
Veröffentlicht: (2024)

ocLTL: LTL Realizability and Synthesis Modulo ω-Categorical Structures
von: Asor, Ohad
Veröffentlicht: (2026)

Finding Connections via Satisfiability Solving
von: Eisenhofer, Clemens, et al.
Veröffentlicht: (2026)

Constraint Learning for Non-confluent Proof Search
von: Rawson, Michael, et al.
Veröffentlicht: (2026)

Lazy Reimplication in Chronological Backtracking
von: Coutelier, Robin, et al.
Veröffentlicht: (2025)

Spanning Matrices via Satisfiability Solving
von: Eisenhofer, Clemens, et al.
Veröffentlicht: (2024)

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols
von: Yatapanage, Nisansala P., et al.
Veröffentlicht: (2023)

On the Completeness of Interpolation Algorithms
von: Hetzl, Stefan, et al.
Veröffentlicht: (2024)

Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics
von: Lyon, Tim S.
Veröffentlicht: (2024)

Completions of Kleene's second model
von: Terwijn, Sebastiaan A.
Veröffentlicht: (2023)

Revisiting Assumptions Ordering in CAR-Based Model Checking
von: Dong, Yibo, et al.
Veröffentlicht: (2024)

Groupoidal Realizability for Intensional Type Theory
von: Speight, Sam
Veröffentlicht: (2024)

Realizability in Semantics-Guided Synthesis Done Eagerly
von: Meyer, Roland, et al.
Veröffentlicht: (2024)

Certificate-Aware Property-Directed Reachability
von: Ferdowsi, Arman, et al.
Veröffentlicht: (2026)

On Solving String Equations via Powers and Parikh Images
von: Eisenhofer, Clemens, et al.
Veröffentlicht: (2026)

SAT-Based Subsumption Resolution
von: Coutelier, Robin, et al.
Veröffentlicht: (2024)

Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
von: André, Étienne, et al.
Veröffentlicht: (2023)

Complete and Terminating Tableau Calculus for Undirected Graph
von: Nishimura, Yuki, et al.
Veröffentlicht: (2024)

Constrained Assumption-Based Argumentation Frameworks
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2026)

Proof-Theoretic Functional Completeness for the Connexive Logic C
von: Ayhan, Sara, et al.
Veröffentlicht: (2025)

Stateful Realizers for Nonstandard Analysis
von: Dinis, Bruno, et al.
Veröffentlicht: (2022)

Some General Completeness Results for Propositionally Quantified Modal Logics
von: Ding, Yifeng, et al.
Veröffentlicht: (2024)