2021/11/23 by Emanuele De Angelis, De Angelis, Emanuele, Fabio Fioravanti +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2111.11819
openalex publication_date 2021/11/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We address the problem of checking the satisfiability of Constrained Horn\nClauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees.\nWe propose a new technique for transforming CHCs defined on ADTs into CHCs\nwhere the arguments of the predicates have only basic types, such as integers\nand booleans. Thus, our technique avoids, during satisfiability checking, the\nexplicit use of proof rules based on induction over the ADTs. The main\nextension over previous techniques for ADT removal is a new transformation\nrule, called differential replacement, which allows us to introduce auxiliary\npredicates, whose definitions correspond to lemmas that are used when making\ninductive proofs. We present an algorithm that performs the automatic removal\nof ADTs by applying the new rule, together with the traditional\nfolding/unfolding rules. We prove that, under suitable hypotheses, the set of\nthe transformed clauses is satisfiable if and only if so is the set of the\noriginal clauses. By an experimental evaluation, we show that the use of the\nnew rule significantly improves the effectiveness of ADT removal. We also show\nthat our approach is competitive with respect to tools that extend CHC solvers\nwith the use of inductive rules.\n