In this paper, we present a clausal logic ofbelief which formalizes beliefs in an extendedclausal jorm of logic. Our aims are to solve therepresentationeil problem of quantified beliefs and to allow an efficient resolution-like proof procedure with controlled granularity to be developed.A levelled intensional scheme that enablesthe clausalization of belief is proposed.An inferential power bounded resolution ruleof beliefs for the formalism is introduced. Theformal semantics of the formalism is defined.A general circumscriptive non-monotonic reasoningsystem for belief revision is described. Finally, a scheme for handling the consistency of beliefs under Tarski's truth definition theoremis developed.