  Recursive definitions of predicates are usually interpreted either
inductively or coinductively. Recently, a more powerful approach has been
proposed, called flexible coinduction, to express a variety of intermediate
interpretations, necessary in some cases to get the correct meaning. We provide
a detailed formal account of an extension of logic programming supporting
flexible coinduction. Syntactically, programs are enriched by coclauses,
clauses with a special meaning used to tune the interpretation of predicates.
As usual, the declarative semantics can be expressed as a fixed point which,
however, is not necessarily the least, nor the greatest one, but is determined
by the coclauses. Correspondingly, the operational semantics is a combination
of standard SLD resolution and coSLD resolution. We prove that the operational
semantics is sound and complete with respect to declarative semantics
restricted to finite comodels. This paper is under consideration for acceptance
in TPLP.
