 The power of the type inference system (refiner) is further augmented by a mechanism of
hints
that helps in synthetizing unifiers in particular situations specified by the user.Matita supports a sophisticated disambiguation strategy 
based on a dialog between the parser and the typechecker.At the interactive level, the system implements a small step execution of structured tactics
allowing a much better management of the proof development, and naturally leading
to more structured and readable scripts.