SE212
Semantic Tableaux
Semantic tableaux is another way of showing an argument is valid. We actually use negations to have everything come to a contradiction.
br
= branching
nb
= nonbranching
 To show an argument is valid, we use a semantic tableau to show that $P_{1},P_{2},…,P_{N},¬Q$ is an inconsistent set of formulas, i.e.

 premise

 premise

 negation of conclusion
 To prove that a set is Inconsistent Formula, just list out the premises and close everything
Examples
$Prove that{b∧c,d,¬(c∧d)}is inconsistent$
To prove that an argument is valid
$a290∣!a290∣!(a450∧bsup)∨a450∧bsup<−>true$
<→ a290  !(a290  a450 & bsup)  a450 & bsup by dm
<→ a290  a450  bsup  !(a290  a450 & bsup)
<→ true by lem
$∣=¬(a290∧a450∧bsup)$
Recognize that the above formula is not a Tautology.