The MJRTY Algorithm
Model checking an instance
Planning the proof
Intermediary assertions
Using the sequent rules
Back to the tutorial pages