Axioms in definitional calculi

Abstract

This paper introduces a restricted form of the axiom rule in calculi of Partial Inductive Definitions 0aiD). The paper argues that in calculi of PIDs the distinction between atomic and non-atomic formulae is not as clear as in traditional sequent calculi. Therefore the common restriction of the axiom rule to the atomic case is not adequate for this type of calculi. A novel proviso for the axiom rule and corresponding provisos for the left and right definition rules are introduced with an accompanying discussion and suggestions for possible applications in the domain of declarative specification of operational behaviour of logic programs.