Artificial intelligent assistant

Issue proving that a formula is valid using semantic tableau I have to prove that a formula in propositional logic is valid. I created a truth table which shows that the formula is valid (a tautology); however I am doing something wrong when trying to prove this using a semantic tableau by creating a semantic tableau of the formula's complement. All leaf nodes should be closed with X as a result of a complementary pair of atoms, but in my attempt all leaf nodes are open as there are no complementary pairs of atoms in any leaf nodes... Any idea what I'm doing wrong here? My semantic tableau: < The alpha and beta rules I used to construct this semantic tableau: <

The $\alpha$ rules are different from the $\beta$ rules. For the $\alpha$ rules, you create a new branch for each of $\alpha_1$ and $\alpha_2$. But for the $\beta$ rules, you don't branch. Rather, you put both $\beta_1$ and $\beta_2$ in the same branch.

If you think about the rules conceptually, and what you are trying to do with this tableaux method this should all makes sense. That is, in general, in a semantic tableaux method you exolore all possible options to make some statement true. Thus, for example, there are two ways to make a statement like $P \lor Q$ true: either $P$ is true, or $Q$ is true. Hence, you create a branch for each of those ways. n the other hand, there is only one way to make $\
eg (P \lor Q)$ true, and that is by setting both $p$ and $Q$ to false. This is why you get both $\
eg P$ and $\
eg Q$ still in the same branch.

Below is a pic of the tree as it should look like:

![enter image description here](

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy 91d64e0d4d321dc722f11ef8641c7eae