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 <[email protected]> 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 <[email protected]> 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 >
