Suggestions for Synproof

The following packages have something in common with the package Synproof. The packages are ordered in decreasing similarity.

Package fitch: LaTeX macros for Fitch-style natural deduction
Package gb4e: Linguistic tools
Package qtree: Draw tree structures
Package paracol: Multiple columns with texts in parallel
Package turnstile: Typeset the (logic) turnstile notation
Package lkproof: LK Proof figure macros
Package expex: Linguistic examples and glosses, with reference capabilities
Package gene-logic: Typeset logic formulae, etc.
Package linguex: Format linguists’ examples
Package arcs: Draw arcs over and under text
Package pst-tree: Trees, using PSTricks
Package pst-asr: Typeset autosegmental representations for linguists
Package pst-tvz: Draw trees with more than one root node, using PSTricks
Package egpeirce: Draw existential graphs invented by Charles S. Peirce
Package logicproof: Box proofs for propositional and predicate logic
Package syllogism: Typeset syllogisms in LaTeX
Package fodot: Helpful commands to work with the FODOT
Package temporal-logic: Symbols for Temporal Logics
Package begriff: Typeset Begriffschrift
Package frege: Typeset fregean Begriffsschrift
Package grundgesetze: Typeset Frege’s Grundgesetze der Arithmetik
Package logictools: Additional tools for typesetting formal logic
Package principia: Notations for typesetting the Principia Mathematica
Package tipauni: Producing Unicode characters with TIPA commands
Package pst-node: Nodes and node connections in PSTricks
Package pst-jtree: Typeset complex trees for linguists
Package prooftrees: Forest-based proof trees (symbolic logic)
Package covington: LaTeX macros for Linguistics
Package fragoli: Macros for constructing complex semantic derivations
Package leipzig: Typeset and index linguistic gloss abbreviations
Package numending: Generates morphological end of units