probset2-sol

CS486 Problem Set 2 DUE: 2/11/03

1.

Solve the exercise on p. 24, items 1, 4, 5, and 8.

(1)

$\begin{displaymath} \begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{q}{\supset }{({... ...ox{(3)}\\ \multicolumn{4}{c}{\mathsf{X} \mbox{(2)}}\end{array}\end{displaymath}$

(4)

$\begin{displaymath} \begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{[{({({p}{\supse... ...eauxAux} \end{array}} \end{tableauxAux} \end{array}}\end{array}\end{displaymath}$

(5)

$\begin{displaymath} \begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{{\neg }{({p}{\w... ...athsf{X} \mbox{(8)}} \end{tableauxAux} \end{array}}\end{array}\end{displaymath}$

(8)

$\begin{displaymath} \begin{array}[t]{lccr}\mbox{(1)}&\mathsf{F}&{({p}{\vee }{({q... ...lumn{4}{c}{\mbox{*}} \end{tableauxAux} \end{array}}\end{array}\end{displaymath}$

$\begin{displaymath} \begin{array}[t]{lccr}\multicolumn{4}{c}{\mbox{*}}\\ \mbox{... ...thsf{X} \mbox{(11)}} \end{tableauxAux} \end{array}}\end{array}\end{displaymath}$

2.

Recall that a tableaux $\mathcal{T}$ is complete if all its branches are either closed or complete, where a branch $\theta$ of a tableaux $\mathcal{T}$ is complete if for every $\alpha$ on $\theta$ both $\alpha_1$ and $\alpha_2$ occur on $\theta$ and if for every $\beta$ on $\theta$ at least one off $\beta_1$ , $\beta_2$ occur on $\theta$ .

We prove that the tableaux method terminates.

We generate an analytic tableaux for the unsigned formula in the following manner. At each stage, we have an ordered dyadic tree $\mathcal{T}_i$ , In the first stage, we construct the tree $\mathcal{T}_1$ , a one-point tree whose origin is $\mathsf{F}~X$ . In the $n^{th}$ stage, we select from $\mathcal{T}_{n-1}$ the left-most branch $\theta$ that is unclosed and incomplete. From this branch, we consider all $\alpha$ on $\theta$ such that either $\alpha_1$ or $\alpha_2$ does not occur on $\theta$ and all $\beta$ on $\theta$ such that neither $\beta_1$ nor $\beta_2$ occur on $\theta$ . We select the $\alpha$ or $\beta$ node that dominates all others. If we select an $\alpha$ node such that $\alpha_1$ does not occur on $\theta$ , then extend $\theta$ by $\alpha_1$ to form $\mathcal{T}_n$ . If we select an $\alpha$ node such that $\alpha_2$ does not occur on $\theta$ , then extend $\theta$ by $\alpha_2$ to form $\mathcal{T}_n$ . If we select $\beta$ node, then extend $\theta$ by $\beta_1$ , $\beta_2$ to form $\mathcal{T}_n$ .

We show that the above method either closes or completes any branch $\theta$ by induction on the ``size'' of the branch. Define $size(\theta)$ as follows:

$\begin{displaymath} size(\theta) = \left\{ \begin{array}{ll} 0 & \mbox{if $\t... ...& \mbox{where $x$\ is the node selected} \end{array} \right. \end{displaymath}$

Note that an incomplete branch necessarily has an $\alpha$ or $\beta$ node selected by the above procedure; furthermore, the degree of an $\alpha$ or $\beta$ node is greater than zero. Hence $size(\theta) > 0$ for any unclosed, incomplete branch.

Suppose $size(\theta) = 0$ . Then $\theta$ is closed or complete.

Suppose $size(\theta) > 0$ . Suppose an $\alpha$ node is selected. In either one or two steps, we must close or complete $\theta:\alpha_1:\alpha_2$ . Note $size(\theta:\alpha_1:\alpha_2) < size(\theta)$ because $deg(\alpha_1) + deg(\alpha_2) < deg(\alpha)$ . Hence, by the induction hypothesis, the method closes or completes the branch. Suppose a $\beta$ node is selected. Then we must close or complete $\theta:\beta_1$ and $\theta:\beta_2$ . Note $size(\theta:\beta_1) < size(\theta)$ because $deg(\beta_1) < deg(\beta)$ ; likewise, $size(\theta:\beta_2) < size(\theta)$ because $deg(\beta_2) < deg(\beta)$ . Hence, by the induction hypothesis, the method closes or completes both branches.

Hence, the method closes or completes any branch. In particular, the method closes or completes the one-point tree whose origin is $\mathsf{F}~X$ . Thus, the tableaux method terminates.

3.

We prove that any downward closed set

satisfying for all signed formulas , $X \in S$ iff $\overline{X} \not\in S$ is a truth set.

Let be a downward closed set satisfying for all signed formulas , $X \in S$ iff $\overline{X} \not\in S$ . We show that satisfies the laws of a truth set:

(0)

Show that for any

, exactly on of

, $\overline{X}$ belongs to

Let be a signed formula. If $X \in S$ , then $\overline{X} \not\in S$ , by the definition of . If $X \not\in S$ , then $\overline{X} \in S$ , by the definition of . Hence, exactly one of , $\overline{X}$ belongs to .

(a)

Show $\alpha \in S$ iff $\alpha_1 \in S$ and $\alpha_2 \in S$ .

Consider $\alpha$ . If $\alpha \in S$ , then $\alpha_1 \in S$ and $\alpha_2 \in S$ , by the definition of downward closed. Suppose $\alpha_1 \in S$ and $\alpha_2 \in S$ . By way of contradiction, assume $\alpha \not\in S$ . By the definition of , $\overline{\alpha} \in S$ . By , $\overline{\alpha}$ is some $\beta$ . Hence $\beta_1 \in S$ or $\beta_2 \in S$ , by the definition of downward closed. Furthermore, by , $\overline{\alpha_1}$ is $\beta_1$ and $\overline{\alpha_2}$ is $\beta_2$ . Thus, $\overline{\alpha_1} \in S$ or $\overline{\alpha_2} \in S$ . If $\overline{\alpha_1} \in S$ , then $\alpha_1 \not\in S$ , by definition of , but contrary to the assumption. If $\overline{\alpha_2} \in S$ , then $\alpha_2 \not\in S$ , by the definition of , but contrary to the assumption. Hence $\alpha \in S$ .

(b)

Show $\beta \in S$ iff $\beta_1 \in S$ or $\beta_2 \in S$ .

Consider $\beta$ . If $\beta \in S$ , then $\beta_1 \in S$ or $\beta_2 \in S$ , by the definition of downward closed. Suppose $\beta_1 \in S$ or $\beta_2 \in S$ . By way of contradiction, assume $\beta \not\in S$ . By the definition of , $\overline{\beta} \in S$ . By , $\overline{\beta}$ is some $\alpha$ . Hence $\alpha_1 \in S$ and $\alpha_2 \in S$ , by the defintion of downward closed. Furthermore, by , $\overline{\beta_1}$ is $\alpha_1$ and $\overline{\beta_2}$ is $\alpha_2$ . Thus, $\overline{\beta_1} \in S$ and $\overline{\beta_2} \in S$ . Hence $\beta_1 \not\in S$ and $\beta_2 \not\in S$ , by the defintion of , but contrary to the assumption. Hence, $\beta \in S$ .

4.

We give a recursive datatype definition for an analytic tableau.

    Form = var: Var + 
           neg: Form + 
           and: Form * Form + 
           or: Form * Form +
           imp: Form * Form
    Sign = t: Unit + f: Unit
    Tableaux = index: Nat *
               sign: Sign *
               form: Form *
               next: (closed: Int + 
                      complete: Unit +
                      alpha: Int * Tableaux + 
                      beta: Int * Tableaux * Tableaux)

Juanita Heyerman 2003-03-03