Title: Complete Cyclic Proof Systems for Inductive Entailments,
Abstract: In this paper we develop cyclic proof systems for the problem of inclusion
between the least sets of models of mutually recursive predicates, when the
ground constraints in the inductive definitions belong to the quantifier-free
fragments of (i) First Order Logic with the canonical Herbrand interpretation
and (ii) Separation Logic, respectively. Inspired by classical
automata-theoretic techniques of proving language inclusion between tree
automata, we give a small set of inference rules, that are proved to be sound
and complete, under certain semantic restrictions, involving the set of
constraints in the inductive system. Moreover, we investigate the decidability
and computational complexity of these restrictions for all the logical
fragments considered and provide a proof search semi-algorithm that becomes a
decision procedure for the entailment problem, for those systems that fulfill
the restrictions.