# Tagged Questions

for subject-specific typesetting involving logic notation.

55 views

### Vertical dots centred in Lemmon style derivation

I would like to center vertical dots in this derivation...I tried with \center but the dots remains in the left. \align can't work in the \ND enviroment. \documentclass{article} \usepackage{ND} \...
35 views

### How to format deduction/equation extending multiple pages?

I'm working on a logic paper that includes a deduction of one of DeMorgan's laws. The proof is Fitch style using Johan Klüwer's 2003 fitch.sty package. It's a long proof and I inevitably end up with a ...
2k views

### How do I get the single turnstile symbol? [duplicate]

I am trying to replicate a logic symbol that looks like \models but has only one horizontal line, and represents a logical deduction. It looks roughly like |-. I have tried Detexify, but it does not ...
211 views

### Typeset simplified ROM circuit diagram using Tikz

I'm trying to typeset the following image using Tikz: I have tried many options, but there doesn't seem to be any good solution doing this an efficient way. My code I used at last: \begin{...
48 views

### Arrow-implication

I'm writing my thesis and I need use a symbol of science implication that looks like or maybe something like but thicker. I'm curious how to generate it. This link How to look up a symbol or ...
8k views

### What is the best package out there to typeset proof trees?

So, I want to typeset some proof trees, i.e. trees of inference rules like those in natural deduction (see diagram below). Which are the best packages that you have found that allow you to do this, ...
76 views

### Function of interpretation by assignment g

How can I make this function in LaTeX: I tried with \Vmatrix as: $\begin{Vmatrix} \bullet \end{Vmatrix}^{\mathscr{M}_i,g}$ but its not the same. If you can help me, I'd appreciate it.
44 views

### Prooftrees logic tree preamble for an example

The following example is out of the documentation of prooftrees (I suppose that an updated version of TeX Live is needed to make use of that package). The problem is that the documentation's .tex file ...
42 views

### How to typeset axiomatic logic proofs in list form?

I'm trying to typeset some axiomatic logic proofs in list form. I have tried to define a new environment such that I could combine the proof environment of the amsthm package with a table, resulting ...
195 views

### lplfitch package : Add line numbering on the left

I am using the package lplfitch to typeset natural deduction proofs in Fitch style. I would like to number the lines on the left side of the vertical bar instead of on the left of the formula? ...
35 views

### How to place two proof trees next to each other with a symbol in between?

I have to typeset a transformation rule for proof trees, created with the bussproofs package. What I need is an implication sign between two proof trees - aligned with the horizontal separation lines ...
341 views

### How to improve my semantic tableau?

I have to typeset some semantic tableaux in my document, looking similar to the example underneath. My first idea was to use tikz for this, so I created the following monster: \documentclass[...
67 views

### How to apply colour options to the contents of TikZ nodes when the content includes \sbox{}\usebox{}?

Thanks to Sašo Živanović for helping to identify the problem which arises as a result of my trying to apply options such as blue or text=blue to nodes within Forest trees which include turnstiles from ...
62 views

### Will prooftrees be able to typeset this?

The tree is split between two pages, and text lines are inserted among some tree lines. The tree looks shifted to the left on the next page because the book is two-sided, but I don't typeset two-sided ...
60 views

### How do you write the double turnstille & its negation in ShareLaTeX?

I think the code for the double turnstile is \vDash and the code for its negation is \nvDash. Neither of these commands work for me in ShareLatex. I enter them, hit recompile and nothing appears. ...
634 views

### Need help with making Logic Trees in qtree/tikz-qtree (i.e. aligning, numbering lines)

I would like to make something similar to the logic tree below. I've tried using tikz-qtree, but I can't figure out how to number every line in the tree. I did however find something else doable in ...
108 views

### How to improve my modal diagram?

I'm writing a paper about modal logic in which I'll quite often need to draw a diagram of 'worlds'. Every world is represented by a dot, which has two labels: the name of the world on one side of the ...
415 views

### How to create a correctly aligned tree proof in logic with 4 branches, columns of line numbers and justifications?

I'm looking for a way to make a Logic Tree with three columns (line number, tree itself and commentary). I've tried using a tikz matrix, and it worked very well, except when I get more than two ...
115 views

### Typesetting horizontal line used in logic

I am trying to typeset a set of rules of a calculs which should look as the examples in the attached pictured. In the example rules are written in classical notation of logic. I especially wonder ...
89 views

### Logicproof dashed boxes for Natural Deduction

I have been using the Logicproof package to write proofs in Fitch style. It creates environments using tabular to make writing proofs less bothersome. I can't seem to figure out how to create a ...
40 views

### Node on the side of a horizontal tree

I am struggling to understand how to put a node on the branch of the first level of a tree of bernoulli trials. When I try to draw it out, the node label in the center of the branch becomes the ...
61 views

### Premise Discharge with vertical dots with bussproof.sty

Is it possible with bussproof.sty package to obtain a discharge of premiss with vertical dots? Ex: With proof.sty package I use \infer* to obtain vertical dots discharge \documentclass[a4paper,12pt,...
114 views

### How do I display verification of propositional logic in this way?

I want to typeset something like the following picture. I came up with \documentclass[oneside,12pt]{article} \usepackage{microtype} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{...
73 views

### special logic gate

How would one go about drawing a logic gate like this one ?
136 views

### Sequent calculus using prooftree [closed]

I am trying to write sequent calculus proofs using the prooftree package like the one on page 58 of this document. How can I do this?
4k views

### How do I put a circle around an operator?

For example, I want to put a circle around \land, just like one can put a circle around + by writing \oplus. Is there a general method to do this?
193 views

### Analytic Tableaux Smullyan's Style

Is there a simple and intuitive way to drawn with latex this kind of tree? I tried to check in the site "LATEX for LOGICIANS", but I can't find this kind of tree, with this kind of layout. Thank you
128 views

### Derivation tree for type evaluations

I’d like to create derivations trees for a type evaluation (dunno what this is exactly called). Basically I want to reproduce this bottom up „tree“ on page 15 from http://lucacardelli.name/papers/...
32 views

### Small labels with proof.sty [duplicate]

Is it possible to obtain small labels with proof.sty? \documentclass[a4paper,12pt,twoside,openright]{book} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage[german,english,italian]{...
104 views

### Assumptions discharge, proof summary and labelling with bussproof

Is it possible with bussproof package obtain this kind of formula-layout?: (1) Assumptions discharge with four vertical dots; (2) Four vertical dots for proof summary; (3) Labelling with a number (...
39k views

### How to draw Venn diagrams (especially: complements) in LaTeX

What I am up to is to write some exercises dealing with logical formulas for my students, like: And the students should draw these formulas on Venn diagrams. At the end of the lesson, I really ...
121 views

### Strict conditional symbol without changing the default font?

Here is how to define \strictif as the strict conditional ⥽ from modal logic. \documentclass{article} \usepackage{lipsum} \usepackage{pxfonts} \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \...
154 views

298 views

### Fitch-Style Predicate Logic Proof

I've been attempting to typeset some predicate logic proofs in the style of Huth and Ryan, and I'm having trouble determining how to display declared variables in the same format. Below is an example ...
86 views

### How to typeset right and left logical projection binary operations in LaTeX?

In his section on Boolean Basics in The Art of Computer Programming Volume 4A, Pre-Fascicle 0B, Donald Knuth introduces notation for right and left logical projections, which appropriately look like ...
53 views

### How can I type Genzen style deduction in LyX?

As a philosophy major student, I'm learning how to use LyX. And I don't know how to type genzen style deduction on LyX. And Is there any good reference for LyX like Peter smith's for LaTeX ...
50 views

### Bisimulation symbol? [duplicate]

Very simple question: I'm looking for the symbol that indicates that two worlds from 2 different Kripke-models are bisimilar, that there is a bisimulation between those two. In most articles a left-...
96 views

### AND-OR Graph from Horn clauses

Does anyone know if there is a way to generate a nice graph from Horn clauses? for example: Ideally, I would like to generate AND-OR graphs like this directly from Horn clauses written in Latex; ...
109 views

### How to detect LuaLaTex inside my .tex file and exclude bits and pieces conditionally

Let me state my "problem" first. When using PdfLateX my .tex file compiles rather swiftly and all is fine. I use TeXStudio and make use of the PDF preview feature. Since my LaTeX fu isn't the ...
189 views

### Tabular derivations with bussproofs [duplicate]

I am trying to typeset derivations in the CCG grammar formalism. These are just derivations as in type theory, but with words as the initial premises. I've tried to typeset them using the bussproof ...
47 views

### changing the logic symbols in lplfitch.sty

I'm using lplfitch.sty to produce Fitch-style natural deduction proofs. I want to use different symbols from the ones that are predefined. Specifically, I want to use \sim instead of \neg for ...
3k views

### How do I write logical iff symbol?

I'm currently hearing a lecture about formal systems (a computer science lecture). The lecturer makes a symbol that is written like overlying < and >: Every time when he draws it, he says "...
79 views

### Putting two derivations on the same line

I'm trying to put two logic derivations on the same line, but I'm having trouble figuring out how to do this. Here is a sample of the code that I'm using: \documentclass{article} \usepackage{...
121 views

### Space created below proof using proof.sty

I'm trying to typeset semantic readings of Gentzen sequent proofs like those shown here. I use the package proof.sty to produce the proofs. However, if I want to put any kind of brackets around a ...
957 views

### Alignments in bussproofs package

I'm using bussproofs and would like my premises always to be left-aligned with the beginning of the inference line. So far when I have a single premise inference, I can only get the premise centered ...
In LaTeX the symbol for material implication is produced by $\to$, but for biconditional ?
### What command to use for reversed $\vDash$?
I want to use a symbol similar to $\vDash$ but reversed (like if it's mirrored against an imaginary vertical line). I cannot find such a symbol anywhere. I have used detexify too but no luck ...