OK, I can see the attachment now. I see what you meant. I think the
simplest way of doing this is to consider successive, non-branching
propositions as being within the same node of the tree. Therefore you can
obtain your tableau by using "parboxes" or "minipages". You might be aware
that in LyX there is a button "Insert box" on the toolbar. This button
creates what in LaTeX is called a "minipage" (you can see this by checking
"View source" in the "View menu"). A minipage is a box of text which is
used whenever you need to put multiple lines of text together as a unit.
For example:
\begin{minipage}{3cm}%
This is the first line.\\
This is the second line.\\
This is the third line.
\end{minipage}
The {3cm} is the width of the box. The '\\' symbol is the end of line.
There must not be any spaces after it.
So you can use this inside nodes in your tree. In my previous examples,
whenever I wrote "node {something}" the text "something" was assumed to be
a single line of text. But you can put a minipage box in the node. For
example:
\begin{tikzpicture}
\node {\begin{minipage}{1cm}%
1.~A\\
2.~B
\end{minipage}}
child {node {\begin{minipage}{1cm}%
3.~C\\
4.~D\\
5.~E
\end{minipage}}}
child {node {\begin{minipage}{1cm}%
6.~F\\
7.~G
\end{minipage}}
child {node {8.~H}}
child {node {9.~I}}};
\end{tikzpicture}
So your example would look like this:
\begin{tikzpicture}
[level distance=2.5cm,
level 1/.style={sibling distance=2cm}]
\node {\begin{minipage}{3cm}%
1.~$\neg (p \lor (p \land q)) \limp p$\\
2.~$p \lor (p \land q)$\\
3.~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.5cm}%
4.~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
5.~$p \land q$\\
6.~$p$\\
7.~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}
and you should put the following definitions in the preamble so you can use
them in all of your tableaux:
\def\lor{\vee}
\def\land{\wedge}
\def\limp{\to}
\def\closed{\times}
However, if you try it, it might not look quite right. You'll notice that
the two child nodes appear aligned at the center of their boxes, rather
than at the top. If, however, you want the top of the children to be
aligned, you need to add the following option to the diagram: "every child
node/.style={anchor=north}". So the code for the whole tableau would be
(adjusting the level distance):
\begin{tikzpicture}
[level distance=1.5cm,
level 1/.style={sibling distance=2cm},
every child node/.style={anchor=north}]
\node {\begin{minipage}{3cm}%
1.~$\neg (p \lor (p \land q)) \limp p$\\
2.~$p \lor (p \land q)$\\
3.~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.5cm}%
4.~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
5.~$p \land q$\\
6.~$p$\\
7.~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}
Finally, if your really want to have the edges start from the exact same
point at the bottom of a node, as shown in your PDF example, you need to
add another option: "every child/.style={parent anchor=south}", resulting
in the following:
\begin{tikzpicture}
[level distance=1.5cm,
level 1/.style={sibling distance=2cm},
every child node/.style={anchor=north},
every child/.style={parent anchor=south}]
\node {\begin{minipage}{3cm}%
1.~$\neg (p \lor (p \land q)) \limp p$\\
2.~$p \lor (p \land q)$\\
3.~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.5cm}%
4.~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
5.~$p \land q$\\
6.~$p$\\
7.~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}
Of course, for other tableaux you'll have to edit the formulae
appropriately. In particular you may have to adjust the distances involved,
the width of the minipages, as well as the level and sibling distances
listed in the options.
I hope this helps.
On Tue, Oct 29, 2013 at 8:01 PM, William Hanson <[email protected]> wrote:
> Oops! Here's the attachment.
>
>
> On Tue, Oct 29, 2013 at 6:58 PM, William Hanson <[email protected]> wrote:
>
>> Ernesto, and the group,
>>
>> Again, Ernesto's many examples of trees are helpful in my quest to create
>> tableau proofs in LyX. But these examples still don't have the exact
>> structure I need.
>>
>> I've attached (to earlier messages) a pdf file containing an example of
>> what I'm seeking, but apparently there is trouble viewing it. I don't
>> understand this, since in trial e-mails I've sent to myself the file can be
>> opened and read using Adobe Reader. I'm using gmail and attaching the file
>> in the usual way. I'll attach it again to this message and hope for better
>> results.
>>
>> Here's a crude attempt to represent what I'm after. (I hope it comes
>> through ungarbled.)
>>
>> not((P or (P & Q)) -->P)
>> P or (P & Q)
>> not P
>> / \
>> / \
>> / \
>> P P & Q
>> x P
>> Q
>> x
>>
>> Each of the seven nodes is a formula of a specified formal language.
>> (In this case it's simple propositional logic.) Notice that there are no
>> lines (vertical or sloping) between any of the nodes except when branching
>> occurs. The only lines in the tree are the sloping ones that indicate
>> branching. It is this feature that I'm unable to create. (I know LyX
>> pretty well, but I know practically nothing about LaTeX.)
>>
>> If I could create trees in which nodes are connected with straight lines
>> only when branching occurs, I'd be well on my way.
>>
>> Bill
>>
>
>
--
Ernesto Posse
Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada
