Theories of partial inductive definitions (PID) constitute a class of logics based on the notion of an inductive definition. Formal systems based on this notion can be used to generalize Horn-logic and naturally allow and suggest extensions which differ in interesting ways from generalizations based on first order predicate calculus. E.g. the notion of completion generated by a calculus of PID and the resulting notion of negation is completely natural and does not require externally motivated procedures such as "negation as failure".
For this reason computational issues arising in these calculi deserve closer inspection. This work discuss a number of finitary theories of PID and analyze the algorithmic and semantical issues that arise in each of them.
There has been significant work on implementing logic programming languages in this setting and we briefly present the programming language and knowledge modeling tool GCLAII in which many of the computational problems discussed arise naturally in practice.
Updated 00-09-08 by