C-N / D Logic Structuralizer

m
w1
w2
w3
w4
w5
w6
ψ

Syntax Trees
preset: light
preset: dark

operator color
(fill, stroke, font)

variable color
(fill, stroke, font)

edge
color

bg
color

avoid
overlaps

Structuralizer

font
height

padding
(left, top, right, bottom)

plain
output

debug
mode

• Input and output fields have play and copy buttons next to them, respectively. Input fields are supporting Undo, Redo, and Enter.
• You may import examples to illustrate input formats. Furthermore, conclusion formulas can be omitted from proof summary steps.
• The syntax tree generator supports special symbols and more operators than the structuralizer, but hides unsupported characters.
• There is a wealth of suitable data at github.com/xamidi/pmGenerator. This is also the source of the importable examples.

Input: Propositional formulas in (1. normal, 2. dotted) Polish notation, or 3. condensed detachment proofs in D-notation, or 4. index-based summaries of such proofs.
Output: Conversion betweeen (1.),(2.). — Generation of infix formulas and syntax trees for (1.),(2.). — Generation of plain or structured universal illustrations for pure C-N-formulas and pure D-proofs.
github.com/xamidi/logic-structuralizer