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.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
>
