  Well-known principles of induction include monotone induction and different
sorts of non-monotone induction such as inflationary induction, induction over
well-founded sets and iterated induction. In this work, we define a logic
formalizing induction over well-founded sets and monotone and iterated
induction. Just as the principle of positive induction has been formalized in
FO(LFP), and the principle of inflationary induction has been formalized in
FO(IFP), this paper formalizes the principle of iterated induction in a new
logic for Non-Monotone Inductive Definitions (ID-logic). The semantics of the
logic is strongly influenced by the well-founded semantics of logic
programming. Our main result concerns the modularity properties of inductive
definitions in ID-logic. Specifically, we formulate conditions under which a
simultaneous definition $\D$ of several relations is logically equivalent to a
conjunction of smaller definitions $\D_1 \land ... \land \D_n$ with disjoint
sets of defined predicates. The difficulty of the result comes from the fact
that predicates $P_i$ and $P_j$ defined in $\D_i$ and $\D_j$, respectively, may
be mutually connected by simultaneous induction. Since logic programming and
abductive logic programming under well-founded semantics are proper fragments
of our logic, our modularity results are applicable there as well.
