for subject-specific typesetting involving logic notation.

learn more… | top users | synonyms

8
votes
3answers
98 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} ...
1
vote
2answers
66 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 ...
-1
votes
1answer
50 views

special logic gate

How would one go about drawing a logic gate like this one ?
2
votes
2answers
83 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 ...
2
votes
1answer
57 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 ...
0
votes
0answers
30 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} ...
2
votes
4answers
53 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 ...
1
vote
1answer
29 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 ...
3
votes
1answer
112 views

Missing $ inserted in a logic function

The error appears at this line: \paragraph{ \neg A \wedge (B \vee C) } How do I repair it?
1
vote
2answers
23 views

Formula after inference with bussproof package

Is it possible obtain a formula as in the picture with bussproof? I tried with \documentclass[a4paper,12pt,twoside,openright]{book} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} ...
3
votes
2answers
41 views

Ho to reduce distance between non monotonic turnstile and its subscript

\documentclass[a4paper,12pt,twoside,openright]{book} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage[german,english,italian]{babel} \newcommand{\nc}{\,\mid\!\sim\,} \begin{document} ...
2
votes
1answer
77 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} ...
6
votes
1answer
182 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 ...
0
votes
0answers
38 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. ...
0
votes
0answers
31 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} ...
0
votes
1answer
70 views

Natural deduction in linear style

Someone know a package that permit to write natural deduction in this linear form with this kind of strokes? Thank you! P.S. The example of ND is from Jan von Plato's book, Elements of logical ...
2
votes
1answer
68 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 ...
3
votes
0answers
42 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 ...
0
votes
0answers
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 ...
2
votes
1answer
107 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?
3
votes
1answer
82 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; ...
2
votes
1answer
90 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 ...
8
votes
1answer
331 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 ...
4
votes
1answer
39 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 ...
4
votes
1answer
62 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} ...
1
vote
1answer
85 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 ...
5
votes
3answers
2k 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 ...
1
vote
2answers
114 views

How to leave spaces in a formula [closed]

I want a space in between the variables in this formula (monadic first order temporal logic). I tried using \, and \hspace{} but both do not seem to work. Can somebody help me out? sample formula: ...
5
votes
3answers
527 views

Latex Bussproofs Package Prooftrees on Same Line

I'd like to know how to put two prooftrees on the same line rather than under/ontop of one another. Is that possible? \documentclass{article} \usepackage{bussproofs} \begin{document} ...
1
vote
1answer
46 views

Prooftree with nodes below other nodes

I require large prooftrees using the bussproofs, but the layouting seems to be not optimal. In particular, the package does not place nodes of the tree below other nodes, which would save a lot of ...
5
votes
1answer
95 views

What bar should be used for definition of (formal) languages?

I wanted to know which standard symbol should be used as a delimiter when recursively defining a (formal) language, such as this fragment of arithmetic expressions : X ::= 0 | 1 | X+X | X*X | I use ...
2
votes
2answers
73 views

Inferences with time stamped steps

What I am trying to achieve is the following: What would be the proper way of achieving the desired output?
1
vote
0answers
158 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? ...
11
votes
3answers
538 views

Looking for a specific symbol used in set theory, can't find on detexify

I'm looking for a specific symbol for typesetting my lecture notes in logic and set theory. The character is used to define a new set from two existing sets alpha and beta (which are ordinals): ...
8
votes
3answers
433 views

Designing a new tuple of Algebra Operators

It's neccessary to have at least two extra tuples of Albera Operators. A minimal tuple is a triple (to_be_subset_eq, meet_operator, join_operator). There are some ideas how to make 2 extra tupes. ...
1
vote
1answer
91 views

Uncommon type of logical tree

I'm trying to reproduce such tree: I know that it was created with Latex, but since I'm a beginner, I really don't know where to start. Would it be possible to create something like that in TkiZ?
10
votes
4answers
562 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 ...
0
votes
0answers
188 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 ...
10
votes
2answers
497 views

Fuzzy logic operator symbols

How can I write in Latex symbols for standard or Łukasiewicz conjunction like these? Thank you
8
votes
2answers
346 views

Space that disappears at the edges (beginning/end) of a math formula

Is there a way to produce a space that disappears at the beginning or end of a math formula? Idea: For the formula-final case, something that looks ahead or takes an obligatory argument might be a ...
4
votes
1answer
490 views

lemmon style proof for logic

Does exist a package for Lemmon style proof in Logic? something like: http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-bau.html thanks
4
votes
2answers
704 views

Logical equivalence vDashv

I need to create a symbol logical equivalence. Contact vDash with appropriate vertical line, but I can not find any. Can you advise?
3
votes
1answer
232 views

Argument diagram (logic)

I need to diagram arguments (Beamer). I've tried to use tikzcd but it doesn't work. How can I draw a diagram as the following one?
9
votes
1answer
182 views

Can I use a written out logical connective, rather than a symbol?

My professor uses these really nice, written out, AND and IMPLIES, etc., symbols and I can't seem to figure out or find how he does it. I would love to use them, rather than \wedge or \land. Is it ...
3
votes
2answers
153 views

Left align text in enumerate

I wish to left align justifications in mathematical/logical reasoning. I am currently in an enumerate tag. I have: a) p or q by fact(10) b) r by negation on (a, 10) c) s by implication(b, 5) . . I ...
4
votes
1answer
471 views

Strange alignment when using tilde as the not operator in logic

I wish to use ~ which has latex symbol: \sim for the negation sign in logic. \sim and \neg are the two most frequent symbols for negation in logic. However, I get a strange looking result if I use ...
8
votes
2answers
85 views

Check equality between colors

Consider the following: \colorlet{mycolour1}{black} AND \colorlet{mycolour2}{black} How do I use a command like \ifthenelse{\equal{mycolour1}{mycolour2}}{TRUE}{FALSE} In other words, how can I ...
6
votes
3answers
27k views

latex symbol for “if and only if” [duplicate]

In LaTeX the symbol for material implication is produced by $\to$, but for biconditional ?
9
votes
3answers
2k views

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 ...
3
votes
1answer
528 views

prooftree from bussproofs package inside “cases” environment

I am using bussproofs package to provide some type proofs. According to bussproofs manual, it is impossible to use prooftree inside math mode. However, I would like to insert prooftree in the cases ...