Definition:Marked Leaf
(Redirected from Definition:Unmarked Leaf)
Jump to navigation
Jump to search
Definition
Let $T$ be a semantic tableau.
Let $t$ be a leaf of $T$.
Then $t$ is marked if and only if it has occurred in Step 3 of the Semantic Tableau Algorithm.
Otherwise, it is called unmarked.
Marked Closed Leaf
A marked leaf $t$ of $T$ is marked closed if and only if its label $\map U t$ contains a complementary pair.
This can be designated by adding to $t$ a second label $\times$.
Marked Open Leaf
A marked leaf $t$ of $T$ is marked open if and only if its label $\map U t$ does not contain a complementary pair.
This can be designated by adding to $t$ a second label $\odot$.
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.2$: Algorithm $2.64$