Forward Countermodel Construction in Modal Logic K