Suggestions for synproof

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

Package gene-logic: Typeset logic formulae, etc.
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 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
Package overword: Parse text
Package rst: Drawing rhetorical structure analysis diagrams in LaTeX
Package textglos: Typeset and index linguistic gloss abbreviations
Package dvgloss: Facilities for setting interlinear glossed text
Package interlinear: A package for creating interlinear glossed texts with customizable formatting
Package linguexx: A tagging-aware package for typesetting linguistic examples and glosses
Package drs: Typeset Discourse Representation Structures (DRS)
Package nnext: Extension for the gb4e package
Package sdrt: Macros for Segmented Discourse Representation Theory
Package simplex: LaTeX macros for linguistics
Package fitch: LaTeX macros for Fitch-style natural deduction
Package turnstile: Typeset the (logic) turnstile notation
Package lkproof: LK Proof figure macros
Package ling-macros: Macros for typesetting formal linguistics
Package semtrans: Transliteration of semitic languages
Package muling: MA Thesis class for the Department of Linguistics, University of Mumbai
Package adtrees: Macros for drawing adpositional trees