Buchumschlag

Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Katsura, Hiroyuki, Kobayashi, Naoki, Sakayori, Ken, Sato, Ryosuke
Format:	Preprint
Veröffentlicht:	2025
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

Catamorphic Abstractions for Constrained Horn Clause Satisfiability
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2024)

On Higher-Order Reachability Games vs May Reachability
von: Asada, Kazuyuki, et al.
Veröffentlicht: (2022)

CTL* Verification and Synthesis using Existential Horn Clauses
von: Carelli, Mishel, et al.
Veröffentlicht: (2024)

HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
von: Jiang, Hongjian, et al.
Veröffentlicht: (2025)

Extensional and Non-extensional Functions as Processes
von: Sakayori, Ken, et al.
Veröffentlicht: (2024)

CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
von: Dobos-Kovács, Mihály, et al.
Veröffentlicht: (2025)

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
von: Somorjai, Márk, et al.
Veröffentlicht: (2024)

Proceedings of the 12th Workshop on Horn Clauses for Verification and Synthesis
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2025)

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
von: Kobayashi, Naoki
Veröffentlicht: (2024)

Wiring the Pi-calculus to Denotational Semantics
von: Sakayori, Ken, et al.
Veröffentlicht: (2026)

Open Horn Type Theory
von: Poernomo, Iman
Veröffentlicht: (2025)

Equational Theorem Proving for Clauses over Strings
von: Kim, Dohan
Veröffentlicht: (2023)

Universal Horn Sentences and the Joint Embedding Property
von: Bodirsky, Manuel, et al.
Veröffentlicht: (2021)

An abstract fixed-point theorem for Horn formula equations
von: Hetzl, Stefan, et al.
Veröffentlicht: (2025)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
von: Kutsia, Temur, et al.
Veröffentlicht: (2024)

Multiple Query Satisfiability of Constrained Horn Clauses
von: De Angelis, Emanuele, et al.
Veröffentlicht: (2022)

Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version)
von: Nishida, Naoki, et al.
Veröffentlicht: (2025)

Partial Quantifier Elimination By Certificate Clauses
von: Goldberg, Eugene
Veröffentlicht: (2020)

On matrix rank function over bounded arithmetics
von: Ken, Eitetsu, et al.
Veröffentlicht: (2023)

Algebraic Reasoning over Relational Structures
von: Jurka, Jan, et al.
Veröffentlicht: (2024)

Rethinking Clause Management for CDCL SAT Solvers
von: Cai, Yalun, et al.
Veröffentlicht: (2026)

Disjoint Partial Enumeration without Blocking Clauses
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2023)

Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms (Full Version)
von: Takahata, Kanta, et al.
Veröffentlicht: (2025)

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

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
von: Habermehl, Peter, et al.
Veröffentlicht: (2024)

Testing for Renamability to Classes of Clause Sets
von: Brandl, Albert, et al.
Veröffentlicht: (2025)

Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
von: Aoto, Takahito, et al.
Veröffentlicht: (2024)

Partial Rewriting and Value Interpretation of Logically Constrained Terms (Full Version)
von: Aoto, Takahito, et al.
Veröffentlicht: (2026)

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses
von: Spallitta, Giuseppe, et al.
Veröffentlicht: (2024)

Extended Resolution Clause Learning via Dual Implication Points
von: Buss, Sam, et al.
Veröffentlicht: (2024)

Rings and Boolean Algebras as Algebraic Theories
von: De Faveri, Arturo
Veröffentlicht: (2025)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
von: Cristiá, Maximiliano, et al.
Veröffentlicht: (2022)

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
von: Bezem, Marc, et al.
Veröffentlicht: (2026)

Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
von: Takahata, Kanta, et al.
Veröffentlicht: (2025)

Efficient Neural Clause-Selection Reinforcement
von: Suda, Martin
Veröffentlicht: (2025)

Applications of Quantified Constraint Solving over the Reals -- Bibliography
von: Ratschan, Stefan
Veröffentlicht: (2012)

Identifying Tractable Quantified Temporal Constraints within Ord-Horn
von: Rydval, Jakub, et al.
Veröffentlicht: (2024)

Automated Analysis of Logically Constrained Rewrite Systems using crest
von: Schöpf, Jonas, et al.
Veröffentlicht: (2025)

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

Automating Boundary Filling in Cubical Type Theories
von: Doré, Maximilian, et al.
Veröffentlicht: (2024)