Copertina

Getting Saturated with Induction

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Hajdu, Márton, Hozzová, Petra, Kovács, Laura, Reger, Giles, Voronkov, Andrei
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

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

Program Synthesis in Saturation
di: Hozzová, Petra, et al.
Pubblicazione: (2024)

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

Term Ordering Diagrams
di: Hajdu, Márton, et al.
Pubblicazione: (2025)

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

The Vampire Diary
di: Bártek, Filip, et al.
Pubblicazione: (2025)

Saturating Sorting without Sorts
di: Georgiou, Pamina, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
di: Bacci, Giorgio, et al.
Pubblicazione: (2025)

Spanning Matrices via Satisfiability Solving
di: Eisenhofer, Clemens, et al.
Pubblicazione: (2024)

Lazy Reimplication in Chronological Backtracking
di: Coutelier, Robin, et al.
Pubblicazione: (2025)

Finding Connections via Satisfiability Solving
di: Eisenhofer, Clemens, et al.
Pubblicazione: (2026)

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

Templates in Rewriting Induction
di: Hagens, Kasper, et al.
Pubblicazione: (2026)

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

Bounded Rewriting Induction for LCSTRSs
di: Hagens, Kasper, et al.
Pubblicazione: (2026)

Induction rules for Transition Algebra
di: Hashimoto, Go
Pubblicazione: (2026)

SAT-Based Subsumption Resolution
di: Coutelier, Robin, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

Vampire
di: Bártek, Filip, et al.
Pubblicazione: (2025)

Circular Induction
di: Lucanu, Dorel, et al.
Pubblicazione: (2026)

Local structure of idempotent algebras I
di: Bulatov, Andrei A.
Pubblicazione: (2020)

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
di: Peled, Romy, et al.
Pubblicazione: (2025)

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

Formal Verification of Parameterized Systems based on Induction
di: Xiu, Jiaqi, et al.
Pubblicazione: (2025)

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

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

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

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

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