Pri vyhodnocovaní vetiev sémantických stromov v modálnej logike sa používajú rôzne pravidlá, ktoré zaručujú správne vyhodnotenie formúl obsahujúcich operátory □ (notácia pre "nutne") a ◇ (notácia pre "možno"). Tu uvádzam niektoré základné pravidlá, ktoré sa používajú pri konštruovaní sémantických stromov v modálnej logike:

1. Ak sa v jednej vetve nachádza formula A a zároveň formula ¬A, tak táto vetva je uzavretá a neexistujú žiadne modely, v ktorých by sa obe formuly mohli splniť súčasne.

2. Ak sa v jednej vetve nachádza formula □A, tak musíme vytvoriť novú vetvu a do nej pridať formulovane A. Táto vetva predstavuje všetky modely, v ktorých platí formula A.

3. Ak sa v jednej vetve nachádza formula ◇A, tak musíme vytvoriť novú vetvu a do nej pridať formulovane A. Táto vetva predstavuje aspoň jeden model, v ktorom platí formula A.

4. Ak sa v jednej vetve nachádza formula ¬□A, tak musíme vytvoriť novú vetvu a do nej pridať formulovane ¬A. Táto vetva predstavuje všetky modely, v ktorých neplatí formula A.

5. Ak sa v jednej vetve nachádza formula ¬◇A, tak musíme vytvoriť novú vetvu a do nej pridať formulovane □¬A. Táto vetva predstavuje všetky modely, v ktorých neplatí formula A.

6. Ak sa v jednej vetve nachádza formula □A a zároveň formula □B, tak môžeme tieto dve formuly zlúčiť do jednej vetvy.

7. Ak sa v jednej vetve nachádza formula ◇A a zároveň formula ◇B, tak môžeme tieto dve formuly zlúčiť do jednej vetvy.

8. Ak sa v jednej vetve nachádza formula □A a zároveň formula ◇B, tak môžeme tieto dve formuly zlúčiť do jednej vetvy.

9. Ak sa v jednej vetve nachádza formula ◇A a zároveň formula □B, tak musíme vytvoriť novú vetvu a do nej pridať formulovane ◇A a □B.

Tieto pravidlá sú základom pre správne konštruovanie sémantických stromov v modálnej logike a umožňujú nám určiť, či daná formula je splniteľná,