A natural deduction approach to dynamic logic