Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

I asked about which logic because that determines which operators you will
need (I've only given you a few in my examples), but also because for some
logics the tableaux are not trees but directed acyclic graphs, (e.g., in
temporal logics). This of course has a big impact on how to draw the
tableaux. It can be done in tikz, but it needs additional constructs that I
have not shown in my previous examples. So the question is whether in your
modal logic the tableau construction rules create loops or not.

Since you want to be able to make your own tableaux you will need to learn
a little bit of LaTeX, as I said before. I will try to put together a mini
crash course on the things that you'll need, but in the end you'll need to
do a bit more than just copy-and-paste in order to get what you want. I'll
post the notes here later on. In the meantime you can try the examples, and
try tweaking bits of the code to see what happens.



On Wed, Nov 6, 2013 at 6:12 PM, William Hanson whan...@umn.edu wrote:

 Ernesto,

 I'm writing a paper using LyX, and I need to insert several specific
 tableaus into it.  Using your numbers:

 1) I do not want to add just *any* tableau example.

 2) I do want to add several specific tableaus containing particular
 formulas.  Probably just five or six such tableaus, each of which would
 occupy ten to twenty lines of text.  (By a line of text, I mean a
 horizontal line across the page in the finished, PDF version.  Such a line
 might of course include characters from more that one branch.  In the
 example called Sample Tableau, attached to an earlier message in this
 string, I count 12 horizontal lines of text in the leftmost branch (not
 counting the slanted lines that indicate branching).)

 3) My original idea was indeed to learn to make my own tableaus so that I
 could accomplish 2.

 When you ask which logic? I assume you're asking which object-language
 formulas will appear (with some additional prefixes and suffixes) as items
 in the tableaus.  The answer is:  first-order modal logic plus a lambda
 operator for predicate abstraction.  That is the object language used in
 the Sample Tableau attachment, except that the formulas in the Sample
 Tableau don't happen to contain any modal connectives.  (The modal
 connectives I'm using are the box and the diamond.)

 I've been pressed for time the last few days, so I haven't yet had a
 chance to try the suggestions you made on Nov 4, or the ones you make today
 (Nov 6).  I'll do so tomorrow and let you know what happens.

 Thanks,

 Bill


 On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.cawrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau example,
 2) add a specific tableau (i.e., a particular example that you have in mind
 with particular formulas), or 3) be able to make your own tableaux. If it
 is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the beginning
 of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
  \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
  child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 \end{center}
 \end{minipage}

 Save this file as tableau_example.tex in the same folder as your LyX
 file.

 3. On LyX, go to the part of your file where 

Re: Logic: Tableau Proofs (trees)

[William Hanson]

No, the tableaus I want to create do not contain any loops.


On Thu, Nov 7, 2013 at 11:01 AM, Ernesto Posse epo...@cs.queensu.ca wrote:

 I asked about which logic because that determines which operators you will
 need (I've only given you a few in my examples), but also because for some
 logics the tableaux are not trees but directed acyclic graphs, (e.g., in
 temporal logics). This of course has a big impact on how to draw the
 tableaux. It can be done in tikz, but it needs additional constructs that I
 have not shown in my previous examples. So the question is whether in your
 modal logic the tableau construction rules create loops or not.

 Since you want to be able to make your own tableaux you will need to learn
 a little bit of LaTeX, as I said before. I will try to put together a mini
 crash course on the things that you'll need, but in the end you'll need to
 do a bit more than just copy-and-paste in order to get what you want. I'll
 post the notes here later on. In the meantime you can try the examples, and
 try tweaking bits of the code to see what happens.



 On Wed, Nov 6, 2013 at 6:12 PM, William Hanson whan...@umn.edu wrote:

 Ernesto,

 I'm writing a paper using LyX, and I need to insert several specific
 tableaus into it.  Using your numbers:

 1) I do not want to add just *any* tableau example.

 2) I do want to add several specific tableaus containing particular
 formulas.  Probably just five or six such tableaus, each of which would
 occupy ten to twenty lines of text.  (By a line of text, I mean a
 horizontal line across the page in the finished, PDF version.  Such a line
 might of course include characters from more that one branch.  In the
 example called Sample Tableau, attached to an earlier message in this
 string, I count 12 horizontal lines of text in the leftmost branch (not
 counting the slanted lines that indicate branching).)

 3) My original idea was indeed to learn to make my own tableaus so that I
 could accomplish 2.

 When you ask which logic? I assume you're asking which object-language
 formulas will appear (with some additional prefixes and suffixes) as items
 in the tableaus.  The answer is:  first-order modal logic plus a lambda
 operator for predicate abstraction.  That is the object language used in
 the Sample Tableau attachment, except that the formulas in the Sample
 Tableau don't happen to contain any modal connectives.  (The modal
 connectives I'm using are the box and the diamond.)

 I've been pressed for time the last few days, so I haven't yet had a
 chance to try the suggestions you made on Nov 4, or the ones you make today
 (Nov 6).  I'll do so tomorrow and let you know what happens.

 Thanks,

 Bill


 On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.cawrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau
 example, 2) add a specific tableau (i.e., a particular example that you
 have in mind with particular formulas), or 3) be able to make your own
 tableaux. If it is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the
 beginning of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
  \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
  child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 

Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

I asked about which logic because that determines which operators you will
need (I've only given you a few in my examples), but also because for some
logics the tableaux are not trees but directed acyclic graphs, (e.g., in
temporal logics). This of course has a big impact on how to draw the
tableaux. It can be done in tikz, but it needs additional constructs that I
have not shown in my previous examples. So the question is whether in your
modal logic the tableau construction rules create loops or not.

Since you want to be able to make your own tableaux you will need to learn
a little bit of LaTeX, as I said before. I will try to put together a mini
crash course on the things that you'll need, but in the end you'll need to
do a bit more than just copy-and-paste in order to get what you want. I'll
post the notes here later on. In the meantime you can try the examples, and
try tweaking bits of the code to see what happens.



On Wed, Nov 6, 2013 at 6:12 PM, William Hanson whan...@umn.edu wrote:

 Ernesto,

 I'm writing a paper using LyX, and I need to insert several specific
 tableaus into it.  Using your numbers:

 1) I do not want to add just *any* tableau example.

 2) I do want to add several specific tableaus containing particular
 formulas.  Probably just five or six such tableaus, each of which would
 occupy ten to twenty lines of text.  (By a line of text, I mean a
 horizontal line across the page in the finished, PDF version.  Such a line
 might of course include characters from more that one branch.  In the
 example called Sample Tableau, attached to an earlier message in this
 string, I count 12 horizontal lines of text in the leftmost branch (not
 counting the slanted lines that indicate branching).)

 3) My original idea was indeed to learn to make my own tableaus so that I
 could accomplish 2.

 When you ask which logic? I assume you're asking which object-language
 formulas will appear (with some additional prefixes and suffixes) as items
 in the tableaus.  The answer is:  first-order modal logic plus a lambda
 operator for predicate abstraction.  That is the object language used in
 the Sample Tableau attachment, except that the formulas in the Sample
 Tableau don't happen to contain any modal connectives.  (The modal
 connectives I'm using are the box and the diamond.)

 I've been pressed for time the last few days, so I haven't yet had a
 chance to try the suggestions you made on Nov 4, or the ones you make today
 (Nov 6).  I'll do so tomorrow and let you know what happens.

 Thanks,

 Bill


 On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.cawrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau example,
 2) add a specific tableau (i.e., a particular example that you have in mind
 with particular formulas), or 3) be able to make your own tableaux. If it
 is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the beginning
 of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
  \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
  child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 \end{center}
 \end{minipage}

 Save this file as tableau_example.tex in the same folder as your LyX
 file.

 3. On LyX, go to the part of your file where 

Re: Logic: Tableau Proofs (trees)

[William Hanson]

No, the tableaus I want to create do not contain any loops.


On Thu, Nov 7, 2013 at 11:01 AM, Ernesto Posse epo...@cs.queensu.ca wrote:

 I asked about which logic because that determines which operators you will
 need (I've only given you a few in my examples), but also because for some
 logics the tableaux are not trees but directed acyclic graphs, (e.g., in
 temporal logics). This of course has a big impact on how to draw the
 tableaux. It can be done in tikz, but it needs additional constructs that I
 have not shown in my previous examples. So the question is whether in your
 modal logic the tableau construction rules create loops or not.

 Since you want to be able to make your own tableaux you will need to learn
 a little bit of LaTeX, as I said before. I will try to put together a mini
 crash course on the things that you'll need, but in the end you'll need to
 do a bit more than just copy-and-paste in order to get what you want. I'll
 post the notes here later on. In the meantime you can try the examples, and
 try tweaking bits of the code to see what happens.



 On Wed, Nov 6, 2013 at 6:12 PM, William Hanson whan...@umn.edu wrote:

 Ernesto,

 I'm writing a paper using LyX, and I need to insert several specific
 tableaus into it.  Using your numbers:

 1) I do not want to add just *any* tableau example.

 2) I do want to add several specific tableaus containing particular
 formulas.  Probably just five or six such tableaus, each of which would
 occupy ten to twenty lines of text.  (By a line of text, I mean a
 horizontal line across the page in the finished, PDF version.  Such a line
 might of course include characters from more that one branch.  In the
 example called Sample Tableau, attached to an earlier message in this
 string, I count 12 horizontal lines of text in the leftmost branch (not
 counting the slanted lines that indicate branching).)

 3) My original idea was indeed to learn to make my own tableaus so that I
 could accomplish 2.

 When you ask which logic? I assume you're asking which object-language
 formulas will appear (with some additional prefixes and suffixes) as items
 in the tableaus.  The answer is:  first-order modal logic plus a lambda
 operator for predicate abstraction.  That is the object language used in
 the Sample Tableau attachment, except that the formulas in the Sample
 Tableau don't happen to contain any modal connectives.  (The modal
 connectives I'm using are the box and the diamond.)

 I've been pressed for time the last few days, so I haven't yet had a
 chance to try the suggestions you made on Nov 4, or the ones you make today
 (Nov 6).  I'll do so tomorrow and let you know what happens.

 Thanks,

 Bill


 On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.cawrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau
 example, 2) add a specific tableau (i.e., a particular example that you
 have in mind with particular formulas), or 3) be able to make your own
 tableaux. If it is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the
 beginning of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
  \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
  child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 

Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

I asked about which logic because that determines which operators you will
need (I've only given you a few in my examples), but also because for some
logics the tableaux are not trees but directed acyclic graphs, (e.g., in
temporal logics). This of course has a big impact on how to draw the
tableaux. It can be done in tikz, but it needs additional constructs that I
have not shown in my previous examples. So the question is whether in your
modal logic the tableau construction rules create loops or not.

Since you want to be able to make your own tableaux you will need to learn
a little bit of LaTeX, as I said before. I will try to put together a mini
crash course on the things that you'll need, but in the end you'll need to
do a bit more than just copy-and-paste in order to get what you want. I'll
post the notes here later on. In the meantime you can try the examples, and
try tweaking bits of the code to see what happens.



On Wed, Nov 6, 2013 at 6:12 PM, William Hanson  wrote:

> Ernesto,
>
> I'm writing a paper using LyX, and I need to insert several specific
> tableaus into it.  Using your numbers:
>
> 1) I do not want to add just *any* tableau example.
>
> 2) I do want to add several specific tableaus containing particular
> formulas.  Probably just five or six such tableaus, each of which would
> occupy ten to twenty lines of text.  (By a line of text, I mean a
> horizontal line across the page in the finished, PDF version.  Such a line
> might of course include characters from more that one branch.  In the
> example called Sample Tableau, attached to an earlier message in this
> string, I count 12 horizontal lines of text in the leftmost branch (not
> counting the slanted lines that indicate branching).)
>
> 3) My original idea was indeed to learn to make my own tableaus so that I
> could accomplish 2.
>
> When you ask "which logic?" I assume you're asking which object-language
> formulas will appear (with some additional prefixes and suffixes) as items
> in the tableaus.  The answer is:  first-order modal logic plus a lambda
> operator for predicate abstraction.  That is the object language used in
> the Sample Tableau attachment, except that the formulas in the Sample
> Tableau don't happen to contain any modal connectives.  (The modal
> connectives I'm using are the box and the diamond.)
>
> I've been pressed for time the last few days, so I haven't yet had a
> chance to try the suggestions you made on Nov 4, or the ones you make today
> (Nov 6).  I'll do so tomorrow and let you know what happens.
>
> Thanks,
>
> Bill
>
>
> On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse wrote:
>
>> Didn't my last suggestions help?
>>
>> I am still unsure about whether you want to 1) add *any* tableau example,
>> 2) add a specific tableau (i.e., a particular example that you have in mind
>> with particular formulas), or 3) be able to make your own tableaux. If it
>> is 1 or 2, which logic? Please clarify.
>>
>> In terms of tools, I'm afraid that there is no tool, to the best of my
>> knowledge, that allows you to make tableaux with absolutely no knowledge of
>> LaTeX. Even if you try to use a drawing program for this purpose, you'll
>> have to write at least the formulas in LaTeX, and it is quite tricky to
>> embed formulas in such drawing tools. So if you want to be able to create
>> your own, I'm afraid you'll have to learn a little bit.
>>
>> As for your example, try doing the following:
>>
>> 1. In LyX: open your file; go to "Document->Settings..->LaTeX Preamble"
>> and enter the following:
>>
>> \usepackage{tikz}
>>
>> \def\land{\wedge}
>> \def\lor{\vee}
>> \def\limp{\to}
>> \def\closed{\times}
>>
>> 2. Open Notepad and enter the following (keep the spaces at the beginning
>> of each line):
>>
>> \begin{minipage}{1\columnwidth}%
>> \begin{center}
>>  \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}{4cm}%
>>  \begin{center}
>>  $1~\neg ((p \lor (p \land q)) \limp p)$\\
>>  $1~p \lor (p \land q)$\\
>>  $1~\neg p $
>>  \end{center}
>>\end{minipage}}
>> child {node {\begin{minipage}{0.5cm}%
>>\begin{center}
>>$1~p$\\
>>$\closed$
>>\end{center}
>>  \end{minipage}}}
>>  child {node {\begin{minipage}{1.5cm}%
>>\begin{center}
>>$1~p \land q$\\
>>$1~p$\\
>>$1~q$\\
>>$\closed$
>>\end{center}
>>  \end{minipage}}};
>> 

Re: Logic: Tableau Proofs (trees)

[William Hanson]

No, the tableaus I want to create do not contain any loops.


On Thu, Nov 7, 2013 at 11:01 AM, Ernesto Posse  wrote:

> I asked about which logic because that determines which operators you will
> need (I've only given you a few in my examples), but also because for some
> logics the tableaux are not trees but directed acyclic graphs, (e.g., in
> temporal logics). This of course has a big impact on how to draw the
> tableaux. It can be done in tikz, but it needs additional constructs that I
> have not shown in my previous examples. So the question is whether in your
> modal logic the tableau construction rules create loops or not.
>
> Since you want to be able to make your own tableaux you will need to learn
> a little bit of LaTeX, as I said before. I will try to put together a mini
> crash course on the things that you'll need, but in the end you'll need to
> do a bit more than just copy-and-paste in order to get what you want. I'll
> post the notes here later on. In the meantime you can try the examples, and
> try tweaking bits of the code to see what happens.
>
>
>
> On Wed, Nov 6, 2013 at 6:12 PM, William Hanson  wrote:
>
>> Ernesto,
>>
>> I'm writing a paper using LyX, and I need to insert several specific
>> tableaus into it.  Using your numbers:
>>
>> 1) I do not want to add just *any* tableau example.
>>
>> 2) I do want to add several specific tableaus containing particular
>> formulas.  Probably just five or six such tableaus, each of which would
>> occupy ten to twenty lines of text.  (By a line of text, I mean a
>> horizontal line across the page in the finished, PDF version.  Such a line
>> might of course include characters from more that one branch.  In the
>> example called Sample Tableau, attached to an earlier message in this
>> string, I count 12 horizontal lines of text in the leftmost branch (not
>> counting the slanted lines that indicate branching).)
>>
>> 3) My original idea was indeed to learn to make my own tableaus so that I
>> could accomplish 2.
>>
>> When you ask "which logic?" I assume you're asking which object-language
>> formulas will appear (with some additional prefixes and suffixes) as items
>> in the tableaus.  The answer is:  first-order modal logic plus a lambda
>> operator for predicate abstraction.  That is the object language used in
>> the Sample Tableau attachment, except that the formulas in the Sample
>> Tableau don't happen to contain any modal connectives.  (The modal
>> connectives I'm using are the box and the diamond.)
>>
>> I've been pressed for time the last few days, so I haven't yet had a
>> chance to try the suggestions you made on Nov 4, or the ones you make today
>> (Nov 6).  I'll do so tomorrow and let you know what happens.
>>
>> Thanks,
>>
>> Bill
>>
>>
>> On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse wrote:
>>
>>> Didn't my last suggestions help?
>>>
>>> I am still unsure about whether you want to 1) add *any* tableau
>>> example, 2) add a specific tableau (i.e., a particular example that you
>>> have in mind with particular formulas), or 3) be able to make your own
>>> tableaux. If it is 1 or 2, which logic? Please clarify.
>>>
>>> In terms of tools, I'm afraid that there is no tool, to the best of my
>>> knowledge, that allows you to make tableaux with absolutely no knowledge of
>>> LaTeX. Even if you try to use a drawing program for this purpose, you'll
>>> have to write at least the formulas in LaTeX, and it is quite tricky to
>>> embed formulas in such drawing tools. So if you want to be able to create
>>> your own, I'm afraid you'll have to learn a little bit.
>>>
>>> As for your example, try doing the following:
>>>
>>> 1. In LyX: open your file; go to "Document->Settings..->LaTeX Preamble"
>>> and enter the following:
>>>
>>> \usepackage{tikz}
>>>
>>> \def\land{\wedge}
>>> \def\lor{\vee}
>>> \def\limp{\to}
>>> \def\closed{\times}
>>>
>>> 2. Open Notepad and enter the following (keep the spaces at the
>>> beginning of each line):
>>>
>>> \begin{minipage}{1\columnwidth}%
>>> \begin{center}
>>>  \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}{4cm}%
>>>  \begin{center}
>>>  $1~\neg ((p \lor (p \land q)) \limp p)$\\
>>>  $1~p \lor (p \land q)$\\
>>>  $1~\neg p $
>>>  \end{center}
>>>\end{minipage}}
>>> child {node {\begin{minipage}{0.5cm}%
>>>\begin{center}
>>>$1~p$\\
>>>$\closed$
>>>\end{center}
>>>  \end{minipage}}}
>>>  child {node {\begin{minipage}{1.5cm}%
>>>\begin{center}
>>>  

Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

Didn't my last suggestions help?

I am still unsure about whether you want to 1) add *any* tableau example,
2) add a specific tableau (i.e., a particular example that you have in mind
with particular formulas), or 3) be able to make your own tableaux. If it
is 1 or 2, which logic? Please clarify.

In terms of tools, I'm afraid that there is no tool, to the best of my
knowledge, that allows you to make tableaux with absolutely no knowledge of
LaTeX. Even if you try to use a drawing program for this purpose, you'll
have to write at least the formulas in LaTeX, and it is quite tricky to
embed formulas in such drawing tools. So if you want to be able to create
your own, I'm afraid you'll have to learn a little bit.

As for your example, try doing the following:

1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble and
enter the following:

\usepackage{tikz}

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\def\closed{\times}

2. Open Notepad and enter the following (keep the spaces at the beginning
of each line):

\begin{minipage}{1\columnwidth}%
\begin{center}
\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}{4cm}%
 \begin{center}
 $1~\neg ((p \lor (p \land q)) \limp p)$\\
 $1~p \lor (p \land q)$\\
 $1~\neg p $
 \end{center}
   \end{minipage}}
child {node {\begin{minipage}{0.5cm}%
   \begin{center}
   $1~p$\\
   $\closed$
   \end{center}
 \end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
   \begin{center}
   $1~p \land q$\\
   $1~p$\\
   $1~q$\\
   $\closed$
   \end{center}
 \end{minipage}}};
\end{tikzpicture}
\end{center}
\end{minipage}

Save this file as tableau_example.tex in the same folder as your LyX file.

3. On LyX, go to the part of your file where you want the tableau. If you
had it in a TeX box, remove it, put the cursor in its place, and go to
Insert-File-Child document Click on Browse... and select
tableau_example.tex.
Click OK.

4. Save your LyX file, and now you should be able to preview it or export
it.


PS: Finally, when posting messages to the mailing list please keep the same
subject line (which you can do by clicking Reply on your e-mail client).
This allows other people who have a similar problem to follow the
conversation. Also, ensure that when replying to help from someone in the
list (including myself), don't forget to CC the mailing list, again, so
that people can follow the conversation and see the possible solutions.




On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:

 Despite much help from Ernesto Posse, for which I'm grateful, and which
 has allowed me to make some progress, I'm still far from being able to
 create tableau proofs in LyX.

 The attached file contains an example of what I want to create.  It's a
 tree, each node of which consists of one or more lines of text (one line
 above another).  These multi-line nodes are connected by slanted lines that
 indicate branching.  The trees do not contain any vertical lines.  There
 are examples in many logic texts, the best source being Melvin Fitting and
 Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.

 I know there are sources on the web that cover related matters (tress in
 linguistics, sequent-calculus proof), but I've not yet found anything
 that's both close to what I need and usable by someone who doesn't know
 LaTeX.

 I've been using LyX for several years.  But since I don't know LaTeX, I'm
 not able to download an existing program and customize it to my needs.

 Bill Hanson





-- 
Ernesto Posse

Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Ernesto,

I'm writing a paper using LyX, and I need to insert several specific
tableaus into it.  Using your numbers:

1) I do not want to add just *any* tableau example.

2) I do want to add several specific tableaus containing particular
formulas.  Probably just five or six such tableaus, each of which would
occupy ten to twenty lines of text.  (By a line of text, I mean a
horizontal line across the page in the finished, PDF version.  Such a line
might of course include characters from more that one branch.  In the
example called Sample Tableau, attached to an earlier message in this
string, I count 12 horizontal lines of text in the leftmost branch (not
counting the slanted lines that indicate branching).)

3) My original idea was indeed to learn to make my own tableaus so that I
could accomplish 2.

When you ask which logic? I assume you're asking which object-language
formulas will appear (with some additional prefixes and suffixes) as items
in the tableaus.  The answer is:  first-order modal logic plus a lambda
operator for predicate abstraction.  That is the object language used in
the Sample Tableau attachment, except that the formulas in the Sample
Tableau don't happen to contain any modal connectives.  (The modal
connectives I'm using are the box and the diamond.)

I've been pressed for time the last few days, so I haven't yet had a chance
to try the suggestions you made on Nov 4, or the ones you make today (Nov
6).  I'll do so tomorrow and let you know what happens.

Thanks,

Bill


On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.ca wrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau example,
 2) add a specific tableau (i.e., a particular example that you have in mind
 with particular formulas), or 3) be able to make your own tableaux. If it
 is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the beginning
 of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
 \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
 child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 \end{center}
 \end{minipage}

 Save this file as tableau_example.tex in the same folder as your LyX
 file.

 3. On LyX, go to the part of your file where you want the tableau. If you
 had it in a TeX box, remove it, put the cursor in its place, and go to
 Insert-File-Child document Click on Browse... and select 
 tableau_example.tex.
 Click OK.

 4. Save your LyX file, and now you should be able to preview it or export
 it.


 PS: Finally, when posting messages to the mailing list please keep the
 same subject line (which you can do by clicking Reply on your e-mail
 client). This allows other people who have a similar problem to follow the
 conversation. Also, ensure that when replying to help from someone in the
 list (including myself), don't forget to CC the mailing list, again, so
 that people can follow the conversation and see the possible solutions.




 On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:

 Despite much help from Ernesto Posse, for which I'm grateful, and which
 has allowed me to make some progress, I'm still far from being able to
 create tableau proofs in LyX.

 The attached file contains an example of what I want to 

Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

Didn't my last suggestions help?

I am still unsure about whether you want to 1) add *any* tableau example,
2) add a specific tableau (i.e., a particular example that you have in mind
with particular formulas), or 3) be able to make your own tableaux. If it
is 1 or 2, which logic? Please clarify.

In terms of tools, I'm afraid that there is no tool, to the best of my
knowledge, that allows you to make tableaux with absolutely no knowledge of
LaTeX. Even if you try to use a drawing program for this purpose, you'll
have to write at least the formulas in LaTeX, and it is quite tricky to
embed formulas in such drawing tools. So if you want to be able to create
your own, I'm afraid you'll have to learn a little bit.

As for your example, try doing the following:

1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble and
enter the following:

\usepackage{tikz}

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\def\closed{\times}

2. Open Notepad and enter the following (keep the spaces at the beginning
of each line):

\begin{minipage}{1\columnwidth}%
\begin{center}
\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}{4cm}%
 \begin{center}
 $1~\neg ((p \lor (p \land q)) \limp p)$\\
 $1~p \lor (p \land q)$\\
 $1~\neg p $
 \end{center}
   \end{minipage}}
child {node {\begin{minipage}{0.5cm}%
   \begin{center}
   $1~p$\\
   $\closed$
   \end{center}
 \end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
   \begin{center}
   $1~p \land q$\\
   $1~p$\\
   $1~q$\\
   $\closed$
   \end{center}
 \end{minipage}}};
\end{tikzpicture}
\end{center}
\end{minipage}

Save this file as tableau_example.tex in the same folder as your LyX file.

3. On LyX, go to the part of your file where you want the tableau. If you
had it in a TeX box, remove it, put the cursor in its place, and go to
Insert-File-Child document Click on Browse... and select
tableau_example.tex.
Click OK.

4. Save your LyX file, and now you should be able to preview it or export
it.


PS: Finally, when posting messages to the mailing list please keep the same
subject line (which you can do by clicking Reply on your e-mail client).
This allows other people who have a similar problem to follow the
conversation. Also, ensure that when replying to help from someone in the
list (including myself), don't forget to CC the mailing list, again, so
that people can follow the conversation and see the possible solutions.




On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:

 Despite much help from Ernesto Posse, for which I'm grateful, and which
 has allowed me to make some progress, I'm still far from being able to
 create tableau proofs in LyX.

 The attached file contains an example of what I want to create.  It's a
 tree, each node of which consists of one or more lines of text (one line
 above another).  These multi-line nodes are connected by slanted lines that
 indicate branching.  The trees do not contain any vertical lines.  There
 are examples in many logic texts, the best source being Melvin Fitting and
 Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.

 I know there are sources on the web that cover related matters (tress in
 linguistics, sequent-calculus proof), but I've not yet found anything
 that's both close to what I need and usable by someone who doesn't know
 LaTeX.

 I've been using LyX for several years.  But since I don't know LaTeX, I'm
 not able to download an existing program and customize it to my needs.

 Bill Hanson





-- 
Ernesto Posse

Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Ernesto,

I'm writing a paper using LyX, and I need to insert several specific
tableaus into it.  Using your numbers:

1) I do not want to add just *any* tableau example.

2) I do want to add several specific tableaus containing particular
formulas.  Probably just five or six such tableaus, each of which would
occupy ten to twenty lines of text.  (By a line of text, I mean a
horizontal line across the page in the finished, PDF version.  Such a line
might of course include characters from more that one branch.  In the
example called Sample Tableau, attached to an earlier message in this
string, I count 12 horizontal lines of text in the leftmost branch (not
counting the slanted lines that indicate branching).)

3) My original idea was indeed to learn to make my own tableaus so that I
could accomplish 2.

When you ask which logic? I assume you're asking which object-language
formulas will appear (with some additional prefixes and suffixes) as items
in the tableaus.  The answer is:  first-order modal logic plus a lambda
operator for predicate abstraction.  That is the object language used in
the Sample Tableau attachment, except that the formulas in the Sample
Tableau don't happen to contain any modal connectives.  (The modal
connectives I'm using are the box and the diamond.)

I've been pressed for time the last few days, so I haven't yet had a chance
to try the suggestions you made on Nov 4, or the ones you make today (Nov
6).  I'll do so tomorrow and let you know what happens.

Thanks,

Bill


On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse epo...@cs.queensu.ca wrote:

 Didn't my last suggestions help?

 I am still unsure about whether you want to 1) add *any* tableau example,
 2) add a specific tableau (i.e., a particular example that you have in mind
 with particular formulas), or 3) be able to make your own tableaux. If it
 is 1 or 2, which logic? Please clarify.

 In terms of tools, I'm afraid that there is no tool, to the best of my
 knowledge, that allows you to make tableaux with absolutely no knowledge of
 LaTeX. Even if you try to use a drawing program for this purpose, you'll
 have to write at least the formulas in LaTeX, and it is quite tricky to
 embed formulas in such drawing tools. So if you want to be able to create
 your own, I'm afraid you'll have to learn a little bit.

 As for your example, try doing the following:

 1. In LyX: open your file; go to Document-Settings..-LaTeX Preamble
 and enter the following:

 \usepackage{tikz}

 \def\land{\wedge}
 \def\lor{\vee}
 \def\limp{\to}
 \def\closed{\times}

 2. Open Notepad and enter the following (keep the spaces at the beginning
 of each line):

 \begin{minipage}{1\columnwidth}%
 \begin{center}
 \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}{4cm}%
  \begin{center}
  $1~\neg ((p \lor (p \land q)) \limp p)$\\
  $1~p \lor (p \land q)$\\
  $1~\neg p $
  \end{center}
\end{minipage}}
 child {node {\begin{minipage}{0.5cm}%
\begin{center}
$1~p$\\
$\closed$
\end{center}
  \end{minipage}}}
 child {node {\begin{minipage}{1.5cm}%
\begin{center}
$1~p \land q$\\
$1~p$\\
$1~q$\\
$\closed$
\end{center}
  \end{minipage}}};
 \end{tikzpicture}
 \end{center}
 \end{minipage}

 Save this file as tableau_example.tex in the same folder as your LyX
 file.

 3. On LyX, go to the part of your file where you want the tableau. If you
 had it in a TeX box, remove it, put the cursor in its place, and go to
 Insert-File-Child document Click on Browse... and select 
 tableau_example.tex.
 Click OK.

 4. Save your LyX file, and now you should be able to preview it or export
 it.


 PS: Finally, when posting messages to the mailing list please keep the
 same subject line (which you can do by clicking Reply on your e-mail
 client). This allows other people who have a similar problem to follow the
 conversation. Also, ensure that when replying to help from someone in the
 list (including myself), don't forget to CC the mailing list, again, so
 that people can follow the conversation and see the possible solutions.




 On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:

 Despite much help from Ernesto Posse, for which I'm grateful, and which
 has allowed me to make some progress, I'm still far from being able to
 create tableau proofs in LyX.

 The attached file contains an example of what I want to 

Re: Logic: Tableau Proofs (trees)

[Ernesto Posse]

Didn't my last suggestions help?

I am still unsure about whether you want to 1) add *any* tableau example,
2) add a specific tableau (i.e., a particular example that you have in mind
with particular formulas), or 3) be able to make your own tableaux. If it
is 1 or 2, which logic? Please clarify.

In terms of tools, I'm afraid that there is no tool, to the best of my
knowledge, that allows you to make tableaux with absolutely no knowledge of
LaTeX. Even if you try to use a drawing program for this purpose, you'll
have to write at least the formulas in LaTeX, and it is quite tricky to
embed formulas in such drawing tools. So if you want to be able to create
your own, I'm afraid you'll have to learn a little bit.

As for your example, try doing the following:

1. In LyX: open your file; go to "Document->Settings..->LaTeX Preamble" and
enter the following:

\usepackage{tikz}

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\def\closed{\times}

2. Open Notepad and enter the following (keep the spaces at the beginning
of each line):

\begin{minipage}{1\columnwidth}%
\begin{center}
\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}{4cm}%
 \begin{center}
 $1~\neg ((p \lor (p \land q)) \limp p)$\\
 $1~p \lor (p \land q)$\\
 $1~\neg p $
 \end{center}
   \end{minipage}}
child {node {\begin{minipage}{0.5cm}%
   \begin{center}
   $1~p$\\
   $\closed$
   \end{center}
 \end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
   \begin{center}
   $1~p \land q$\\
   $1~p$\\
   $1~q$\\
   $\closed$
   \end{center}
 \end{minipage}}};
\end{tikzpicture}
\end{center}
\end{minipage}

Save this file as "tableau_example.tex" in the same folder as your LyX file.

3. On LyX, go to the part of your file where you want the tableau. If you
had it in a TeX box, remove it, put the cursor in its place, and go to
"Insert->File->Child document...". Click on "Browse..." and select
"tableau_example.tex".
Click OK.

4. Save your LyX file, and now you should be able to preview it or export
it.


PS: Finally, when posting messages to the mailing list please keep the same
subject line (which you can do by clicking "Reply" on your e-mail client).
This allows other people who have a similar problem to follow the
conversation. Also, ensure that when replying to help from someone in the
list (including myself), don't forget to CC the mailing list, again, so
that people can follow the conversation and see the possible solutions.




On Mon, Nov 4, 2013 at 10:13 PM, William Hanson  wrote:

> Despite much help from Ernesto Posse, for which I'm grateful, and which
> has allowed me to make some progress, I'm still far from being able to
> create tableau proofs in LyX.
>
> The attached file contains an example of what I want to create.  It's a
> tree, each node of which consists of one or more lines of text (one line
> above another).  These multi-line nodes are connected by slanted lines that
> indicate branching.  The trees do not contain any vertical lines.  There
> are examples in many logic texts, the best source being Melvin Fitting and
> Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.
>
> I know there are sources on the web that cover related matters (tress in
> linguistics, sequent-calculus proof), but I've not yet found anything
> that's both close to what I need and usable by someone who doesn't know
> LaTeX.
>
> I've been using LyX for several years.  But since I don't know LaTeX, I'm
> not able to download an existing program and customize it to my needs.
>
> Bill Hanson
>
>
>


-- 
Ernesto Posse

Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Ernesto,

I'm writing a paper using LyX, and I need to insert several specific
tableaus into it.  Using your numbers:

1) I do not want to add just *any* tableau example.

2) I do want to add several specific tableaus containing particular
formulas.  Probably just five or six such tableaus, each of which would
occupy ten to twenty lines of text.  (By a line of text, I mean a
horizontal line across the page in the finished, PDF version.  Such a line
might of course include characters from more that one branch.  In the
example called Sample Tableau, attached to an earlier message in this
string, I count 12 horizontal lines of text in the leftmost branch (not
counting the slanted lines that indicate branching).)

3) My original idea was indeed to learn to make my own tableaus so that I
could accomplish 2.

When you ask "which logic?" I assume you're asking which object-language
formulas will appear (with some additional prefixes and suffixes) as items
in the tableaus.  The answer is:  first-order modal logic plus a lambda
operator for predicate abstraction.  That is the object language used in
the Sample Tableau attachment, except that the formulas in the Sample
Tableau don't happen to contain any modal connectives.  (The modal
connectives I'm using are the box and the diamond.)

I've been pressed for time the last few days, so I haven't yet had a chance
to try the suggestions you made on Nov 4, or the ones you make today (Nov
6).  I'll do so tomorrow and let you know what happens.

Thanks,

Bill


On Wed, Nov 6, 2013 at 12:46 PM, Ernesto Posse  wrote:

> Didn't my last suggestions help?
>
> I am still unsure about whether you want to 1) add *any* tableau example,
> 2) add a specific tableau (i.e., a particular example that you have in mind
> with particular formulas), or 3) be able to make your own tableaux. If it
> is 1 or 2, which logic? Please clarify.
>
> In terms of tools, I'm afraid that there is no tool, to the best of my
> knowledge, that allows you to make tableaux with absolutely no knowledge of
> LaTeX. Even if you try to use a drawing program for this purpose, you'll
> have to write at least the formulas in LaTeX, and it is quite tricky to
> embed formulas in such drawing tools. So if you want to be able to create
> your own, I'm afraid you'll have to learn a little bit.
>
> As for your example, try doing the following:
>
> 1. In LyX: open your file; go to "Document->Settings..->LaTeX Preamble"
> and enter the following:
>
> \usepackage{tikz}
>
> \def\land{\wedge}
> \def\lor{\vee}
> \def\limp{\to}
> \def\closed{\times}
>
> 2. Open Notepad and enter the following (keep the spaces at the beginning
> of each line):
>
> \begin{minipage}{1\columnwidth}%
> \begin{center}
> \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}{4cm}%
>  \begin{center}
>  $1~\neg ((p \lor (p \land q)) \limp p)$\\
>  $1~p \lor (p \land q)$\\
>  $1~\neg p $
>  \end{center}
>\end{minipage}}
> child {node {\begin{minipage}{0.5cm}%
>\begin{center}
>$1~p$\\
>$\closed$
>\end{center}
>  \end{minipage}}}
> child {node {\begin{minipage}{1.5cm}%
>\begin{center}
>$1~p \land q$\\
>$1~p$\\
>$1~q$\\
>$\closed$
>\end{center}
>  \end{minipage}}};
> \end{tikzpicture}
> \end{center}
> \end{minipage}
>
> Save this file as "tableau_example.tex" in the same folder as your LyX
> file.
>
> 3. On LyX, go to the part of your file where you want the tableau. If you
> had it in a TeX box, remove it, put the cursor in its place, and go to
> "Insert->File->Child document...". Click on "Browse..." and select 
> "tableau_example.tex".
> Click OK.
>
> 4. Save your LyX file, and now you should be able to preview it or export
> it.
>
>
> PS: Finally, when posting messages to the mailing list please keep the
> same subject line (which you can do by clicking "Reply" on your e-mail
> client). This allows other people who have a similar problem to follow the
> conversation. Also, ensure that when replying to help from someone in the
> list (including myself), don't forget to CC the mailing list, again, so
> that people can follow the conversation and see the possible solutions.
>
>
>
>
> On Mon, Nov 4, 2013 at 10:13 PM, William Hanson  wrote:
>
>> Despite much help from Ernesto Posse, for which I'm grateful, and which
>> has allowed me to make some progress, I'm still far 

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Scott,

Yes, what a good idea.  Here are two examples of what I've been able to do
so far.

In both of the following examples I've copied the code directly out of the
TeX Code box which I got from the Insert menu on the LyX toolbar.

*First example*:  It would be perfect if it did not have those vertical
lines in it.

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\begin{tikzpicture}
\node {$1\neg ((p \lor (p \land q)) \limp p)$}
child {node {$ 1 p \lor (p \land q)$}
child {node {$1 \neg p $}
child {node {$1 \ p $}}
child {node {$1 p \land q$}
child {node {$1 p $}
child {node {$1 q $}};
\end{tikzpicture}

*Second example*: It would be perfect if the top three lines of text were
centered over the large inverted vee that indicates branching, and if the
latter were the same length on both legs.

def\lor{\vee}
\def\land{\wedge}
\def\limp{\to}
\def\closed{\times}
\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}{5cm}%
1 ~$\neg ((p \lor (p \land q)) \limp p)$\\
1 ~$p \lor (p \land q)$\\
1 ~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.6cm}%
1 ~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
1 ~$p \land q$\\
1 ~$p$\\
1 ~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}

There they are.  Any Suggestions?

Bill



On Mon, Nov 4, 2013 at 9:50 PM, Scott Kostyshak skost...@lyx.org wrote:

 Hi Bill,

 Have you made an attempt? Could you share it with us?

 Scott

 On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:
  Despite much help from Ernesto Posse, for which I'm grateful, and which
 has
  allowed me to make some progress, I'm still far from being able to create
  tableau proofs in LyX.
 
  The attached file contains an example of what I want to create.  It's a
  tree, each node of which consists of one or more lines of text (one line
  above another).  These multi-line nodes are connected by slanted lines
 that
  indicate branching.  The trees do not contain any vertical lines.  There
 are
  examples in many logic texts, the best source being Melvin Fitting and
  Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.
 
  I know there are sources on the web that cover related matters (tress in
  linguistics, sequent-calculus proof), but I've not yet found anything
 that's
  both close to what I need and usable by someone who doesn't know LaTeX.
 
  I've been using LyX for several years.  But since I don't know LaTeX, I'm
  not able to download an existing program and customize it to my needs.
 
  Bill Hanson
 
 

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

On Tue, Nov 5, 2013 at 11:16 AM, William Hanson whan...@umn.edu wrote:

 There they are.  Any Suggestions?

 Bill

Thanks Bill. I don't know much tikz to help, but hopefully someone who
does will come along. This might also be a good question for
tex.stackexchange.com.

Best of luck,

Scott

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Scott,

Yes, what a good idea.  Here are two examples of what I've been able to do
so far.

In both of the following examples I've copied the code directly out of the
TeX Code box which I got from the Insert menu on the LyX toolbar.

*First example*:  It would be perfect if it did not have those vertical
lines in it.

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\begin{tikzpicture}
\node {$1\neg ((p \lor (p \land q)) \limp p)$}
child {node {$ 1 p \lor (p \land q)$}
child {node {$1 \neg p $}
child {node {$1 \ p $}}
child {node {$1 p \land q$}
child {node {$1 p $}
child {node {$1 q $}};
\end{tikzpicture}

*Second example*: It would be perfect if the top three lines of text were
centered over the large inverted vee that indicates branching, and if the
latter were the same length on both legs.

def\lor{\vee}
\def\land{\wedge}
\def\limp{\to}
\def\closed{\times}
\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}{5cm}%
1 ~$\neg ((p \lor (p \land q)) \limp p)$\\
1 ~$p \lor (p \land q)$\\
1 ~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.6cm}%
1 ~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
1 ~$p \land q$\\
1 ~$p$\\
1 ~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}

There they are.  Any Suggestions?

Bill



On Mon, Nov 4, 2013 at 9:50 PM, Scott Kostyshak skost...@lyx.org wrote:

 Hi Bill,

 Have you made an attempt? Could you share it with us?

 Scott

 On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:
  Despite much help from Ernesto Posse, for which I'm grateful, and which
 has
  allowed me to make some progress, I'm still far from being able to create
  tableau proofs in LyX.
 
  The attached file contains an example of what I want to create.  It's a
  tree, each node of which consists of one or more lines of text (one line
  above another).  These multi-line nodes are connected by slanted lines
 that
  indicate branching.  The trees do not contain any vertical lines.  There
 are
  examples in many logic texts, the best source being Melvin Fitting and
  Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.
 
  I know there are sources on the web that cover related matters (tress in
  linguistics, sequent-calculus proof), but I've not yet found anything
 that's
  both close to what I need and usable by someone who doesn't know LaTeX.
 
  I've been using LyX for several years.  But since I don't know LaTeX, I'm
  not able to download an existing program and customize it to my needs.
 
  Bill Hanson
 
 

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

On Tue, Nov 5, 2013 at 11:16 AM, William Hanson whan...@umn.edu wrote:

 There they are.  Any Suggestions?

 Bill

Thanks Bill. I don't know much tikz to help, but hopefully someone who
does will come along. This might also be a good question for
tex.stackexchange.com.

Best of luck,

Scott

Re: Logic: Tableau Proofs (trees)

[William Hanson]

Scott,

Yes, what a good idea.  Here are two examples of what I've been able to do
so far.

In both of the following examples I've copied the code directly out of the
TeX Code box which I got from the Insert menu on the LyX toolbar.

*First example*:  It would be perfect if it did not have those vertical
lines in it.

\def\land{\wedge}
\def\lor{\vee}
\def\limp{\to}
\begin{tikzpicture}
\node {$1\neg ((p \lor (p \land q)) \limp p)$}
child {node {$ 1 p \lor (p \land q)$}
child {node {$1 \neg p $}
child {node {$1 \ p $}}
child {node {$1 p \land q$}
child {node {$1 p $}
child {node {$1 q $}};
\end{tikzpicture}

*Second example*: It would be perfect if the top three lines of text were
centered over the large inverted vee that indicates branching, and if the
latter were the same length on both legs.

def\lor{\vee}
\def\land{\wedge}
\def\limp{\to}
\def\closed{\times}
\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}{5cm}%
1 ~$\neg ((p \lor (p \land q)) \limp p)$\\
1 ~$p \lor (p \land q)$\\
1 ~$\neg p$
\end{minipage}}
child {node {\begin{minipage}{0.6cm}%
1 ~$p$\\
$\closed$
\end{minipage}}}
child {node {\begin{minipage}{1.5cm}%
1 ~$p \land q$\\
1 ~$p$\\
1 ~$q$\\
$\closed$
\end{minipage}}};
\end{tikzpicture}

There they are.  Any Suggestions?

Bill



On Mon, Nov 4, 2013 at 9:50 PM, Scott Kostyshak  wrote:

> Hi Bill,
>
> Have you made an attempt? Could you share it with us?
>
> Scott
>
> On Mon, Nov 4, 2013 at 10:13 PM, William Hanson  wrote:
> > Despite much help from Ernesto Posse, for which I'm grateful, and which
> has
> > allowed me to make some progress, I'm still far from being able to create
> > tableau proofs in LyX.
> >
> > The attached file contains an example of what I want to create.  It's a
> > tree, each node of which consists of one or more lines of text (one line
> > above another).  These multi-line nodes are connected by slanted lines
> that
> > indicate branching.  The trees do not contain any vertical lines.  There
> are
> > examples in many logic texts, the best source being Melvin Fitting and
> > Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.
> >
> > I know there are sources on the web that cover related matters (tress in
> > linguistics, sequent-calculus proof), but I've not yet found anything
> that's
> > both close to what I need and usable by someone who doesn't know LaTeX.
> >
> > I've been using LyX for several years.  But since I don't know LaTeX, I'm
> > not able to download an existing program and customize it to my needs.
> >
> > Bill Hanson
> >
> >
>

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

On Tue, Nov 5, 2013 at 11:16 AM, William Hanson  wrote:

> There they are.  Any Suggestions?
>
> Bill

Thanks Bill. I don't know much tikz to help, but hopefully someone who
does will come along. This might also be a good question for
tex.stackexchange.com.

Best of luck,

Scott

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

Hi Bill,

Have you made an attempt? Could you share it with us?

Scott

On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:
 Despite much help from Ernesto Posse, for which I'm grateful, and which has
 allowed me to make some progress, I'm still far from being able to create
 tableau proofs in LyX.

 The attached file contains an example of what I want to create.  It's a
 tree, each node of which consists of one or more lines of text (one line
 above another).  These multi-line nodes are connected by slanted lines that
 indicate branching.  The trees do not contain any vertical lines.  There are
 examples in many logic texts, the best source being Melvin Fitting and
 Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.

 I know there are sources on the web that cover related matters (tress in
 linguistics, sequent-calculus proof), but I've not yet found anything that's
 both close to what I need and usable by someone who doesn't know LaTeX.

 I've been using LyX for several years.  But since I don't know LaTeX, I'm
 not able to download an existing program and customize it to my needs.

 Bill Hanson

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

Hi Bill,

Have you made an attempt? Could you share it with us?

Scott

On Mon, Nov 4, 2013 at 10:13 PM, William Hanson whan...@umn.edu wrote:
 Despite much help from Ernesto Posse, for which I'm grateful, and which has
 allowed me to make some progress, I'm still far from being able to create
 tableau proofs in LyX.

 The attached file contains an example of what I want to create.  It's a
 tree, each node of which consists of one or more lines of text (one line
 above another).  These multi-line nodes are connected by slanted lines that
 indicate branching.  The trees do not contain any vertical lines.  There are
 examples in many logic texts, the best source being Melvin Fitting and
 Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.

 I know there are sources on the web that cover related matters (tress in
 linguistics, sequent-calculus proof), but I've not yet found anything that's
 both close to what I need and usable by someone who doesn't know LaTeX.

 I've been using LyX for several years.  But since I don't know LaTeX, I'm
 not able to download an existing program and customize it to my needs.

 Bill Hanson

Re: Logic: Tableau Proofs (trees)

[Scott Kostyshak]

Hi Bill,

Have you made an attempt? Could you share it with us?

Scott

On Mon, Nov 4, 2013 at 10:13 PM, William Hanson  wrote:
> Despite much help from Ernesto Posse, for which I'm grateful, and which has
> allowed me to make some progress, I'm still far from being able to create
> tableau proofs in LyX.
>
> The attached file contains an example of what I want to create.  It's a
> tree, each node of which consists of one or more lines of text (one line
> above another).  These multi-line nodes are connected by slanted lines that
> indicate branching.  The trees do not contain any vertical lines.  There are
> examples in many logic texts, the best source being Melvin Fitting and
> Richard Mendelsohn, First-Order Modal Logic, Kluwer, 1999.
>
> I know there are sources on the web that cover related matters (tress in
> linguistics, sequent-calculus proof), but I've not yet found anything that's
> both close to what I need and usable by someone who doesn't know LaTeX.
>
> I've been using LyX for several years.  But since I don't know LaTeX, I'm
> not able to download an existing program and customize it to my needs.
>
> Bill Hanson
>
>