1. Resolution
2. Modal tautologies
3. LTL-tautologies
4. Buchi automaton
5. (optional) Buchi automaton + LTL