Deduction search in calculi of general type

Some ideas and methods of the automatization of proofs are applied to an analysis of heuristics processes. The general theory of calculuses is chosen as a tool of the analysis. Most of the mathematical results are formulated for Post canonical systems.