Foundation of logic programming based on inductive definition

A logical system of inference rules intended to give the foundation of logic programs is presented. The distinguished point of the approach taken here is the application of the theory of inductive definitions, which allows us to uniformly treat various kinds of induction schema and also allows us to regardnegation as failure as a kind of induction schema. This approach corresponds to the so-called least fixpoint semantics. Moreover, in our formalism, logic programs are extended so that a condition of a clause may be any first-order formula. This makes it possible to write a quantified specification as a logic program. It also makes the class of induction schemata much larger to include the usual course-of-values inductions.