Several indexing methods are based on bit-matrix representations of clauses in a procedure. They are field encoding, superimposed coding with embedded position and variables, and superimposed coding with external variables [HM89].
All these are based on the principle of n-in-m-coding which is described in the next section.