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.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 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
>>
>
>
--
Ernesto Posse
Modelling and Analysis in Software Engineering
School of Computing
Queen's University - Kingston, Ontario, Canada
