Catamorphic Abstractions for Constrained Horn Clause Satisfiability

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi +1

Catamorphisms are functions that are recursively defined on list and trees and, in general, on Algebraic Data Types (ADTs), and are often used to compute suitable abstractions of p…