What falsifies a node in a semantic tree?

Question

With set of Atoms, A = {p1, p2, p3}, and a formula in CNF, let's say (~p1 & ~p2) OR (~p1 & p2 & p3) OR (~p2 & p3), if we draw a semantic Tree for this formula, what will falsify any node in the tree? I know the definition of a failure node and also of inference nodes. What I am trying to understand is, what is the ACTUAL operation at the node as a result of which it will be falsified. Is it an AND of two branches? Is it an OR of two branches?

Answer 1

In order to prove a formula $A$ with Semantic trees, we have to start with $¬A$.

Then we apply the rules to "decompose" the formula : the choice of the rule is dictated by the main connective.

Thus, if we arrive at a node with a conjunction $(A_1 \land A_2)$ we have to apply the rule for $\land$ adding to the node a branch with both formulas $A_1$ and $A_2$.

If instead we have a node with a disjunction $(A_1 \lor A_2)$, we have to add two branches with $A_1$ and $A_2$ respectively.

To show that a node $A$ is unsatisfiable, we have to check that all branches starting from that nodes close i.e. that they contains both $B$ and $¬B$ for some formula $B$.