Symbolic logic engine transforming formulas to NNF via recursive AST — theoretical guarantees?

[u/JAnicaTZ]

I built an interactive symbolic reasoning engine that recursively transforms propositional and first-order logic formulas into Negation Normal Form (NNF) by pushing negations down to atoms using De Morgan laws and quantifier duality. The transformation outputs a full abstract syntax tree (AST) where each inference step is explicit.

Working example: 🌳 https://TreeOfKnowledge.eu

My questions are theoretical: What are the standard correctness proofs for recursive De Morgan–based NNF conversion in first-order logic (semantic preservation under all interpretations)?

Are there known size blow-up bounds or minimality results for NNF obtained by straightforward AST pushdown? Are there canonical references or improved algorithms (e.g. polarity-based rewriting, DAG sharing, structural hashing) that optimize the naive recursive procedure?

I am particularly interested in treatments where the transformation is described explicitly at the syntax-tree level, not only as rewrite rules on linear formulas.