A Constraint Oriented Proof Methodology Based on Modal Transition Systems