Flexible coinductive logic programming

TL;DR

This paper introduces flexible coinductive logic programming, an extension that allows intermediate interpretations of recursive predicates through coclauses, enhancing expressiveness beyond traditional inductive or coinductive semantics.

Contribution

It formalizes a new logic programming framework supporting flexible coinduction with coclauses, and proves soundness and completeness of its operational semantics.

Findings

Supports intermediate predicate interpretations via coclauses

Operates with combined SLD and coSLD resolution

Ensures soundness and completeness for finite comodels

Abstract

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.