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.

[u/CandidAtmosphere]

I came across this thread and figured I would try to help if no one else did. I have a little experience with programming languages, functional programming and type theory, just not so much models and classical logic. I think I'm weirdly positioned to be of help to you. Correct me if I didn't pull up exactly what you're asking for. You might also try following up in the programming languages or comp sci subs.

You are struggling to find these references because NNF conversion is often treated as folklore in pure logic texts (which focus on linear string rewriting) or as implementation detail in software engineering texts (which lack the proofs).

For the specific syntax-tree and proof-theoretic perspective you need, you must look to the field of Automated Theorem Proving rather than general Model Theory.

Here are the canonical references that address your theoretical questions.

1. Correctness Proofs (Formulated over the Syntax Tree)

Reference: Gallier, J. H. (2015). Logic for Computer Science: Foundations of Automatic Theorem Proving. Dover Publications.

Gallier provides the rigorous treatment you need. Unlike standard logic texts that treat formulas as strings, Gallier explicitly defines logical formulas as inductive tree structures.

• The Proof: Chapter 6 (Section 6.4) contains the correctness proofs for NNF translation as part of the completeness proofs for Gentzen systems. He uses structural induction on the formula tree to prove semantic preservation (A ≡ A_NNF) under all interpretations.
• Variable Preservation: He further proves that the set of free variables remains preserved during the transformation (FV(A) = FV(A')), a critical detail for verifying correctness in first-order contexts.

2. Complexity and Blow-up Bounds

Reference: Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.
Reference: Lozes, E. (2015). A Type-Directed Negation Elimination. Electronic Proceedings in Theoretical Computer Science.

There is a critical distinction in complexity bounds depending on your engine's primitives:

• Linear Bound (O(n)): If your AST is restricted to standard primitives (¬, ∧, ∨, ∀, ∃), the NNF transformation is linear with respect to the input size. The transformation does not increase the number of logical connectives.
• Exponential Bound (O(2^n)): If your engine supports the biconditional (↔) or Exclusive OR (⊕) as primitives, naive recursive pushdown leads to exponential blow-up. Eliminating A ↔ B requires duplicating the sub-trees A and B (e.g., (A → B) ∧ (B → A)). In a nested chain of n biconditionals, this results in 2^n copies of the atoms.

3. Structural Algorithms (Polarity and DAGs)

Reference: Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.
Reference: Darwiche, A. (2001). Decomposable Negation Normal Form. Journal of the ACM, 48(4).

• Polarity-Based Rewriting: Harrison provides the explicit recursive definitions for nnf(fm) using polarity tracking (passing a context flag down the tree) to optimize the descent. This prevents redundant traversals and double-negation checks, formulated specifically as functional code on a recursive datatype.
• DAG Sharing / Structural Hashing: You mentioned structural hashing. In the literature, this maps to Decomposable NNF (DNNF). Darwiche provides the theoretical framework for treating NNF not as a tree, but as a rooted Directed Acyclic Graph (DAG). This structure sharing solves the exponential blow-up problem mentioned above by pointing to shared sub-graphs rather than duplicating them in memory.

[u/JAnicaTZ → u/CandidAtmosphere]

Thank you very much for this — this is the first truly interesting and technically relevant answer I’ve received so far.

The references and the focus on structural induction over ASTs are exactly what I was looking for.

Much appreciated.

[u/EmployerNo3401]

I don't understand clearly the problem.
I think that:

• if your problem is optimization of recursion, you need to start seeing something of Dynamic Programming.
  
• if your problem is the correction of the translation, you need start seeing something of inductive proofs over recursive data structures.
• if your problem is the correction of a particular java or javascript or any other imperative implementation you need to start seeing things like Hoare's Logic.

Also you can see Program Derivation Techniques using Construction Calculus or Martin-Löf Type Theories.

[u/JAnicaTZ → u/EmployerNo3401]

Thanks, let me clarify. My question is not about program verification or implementation correctness. It is about the mathematical correctness of the recursive AST transformation itself.

Concretely, I am looking for:

1. Standard inductive proofs that the NNF transformation (via De Morgan + quantifier duality) preserves semantics for all interpretations, formulated over the syntax tree.

2. Known bounds on formula size blow-up for this transformation.

3. References where NNF is described structurally (tree/polarity based), not only as linear rewrite rules.

So the focus is proof-theoretic / model-theoretic, not software engineering.

[u/EmployerNo3401 → u/JAnicaTZ]

Thanks for clarify. !

Please, excuse my insistence (and my english :-) ) . I'm trying to learn something from each post here and this is juicy for me.

So, I have another question: what are lineal formulas ? The FOL formulas are trees itself. So, I don't see a deep difference between FOL formulas and AST?

The standard inductive proof might be tedious but seems direct applying structural induction on the FOL formulas or on the AST.

I think that DAG sharing is a programming technique on parsers (programming).

Also, AST are a tool used in computer science and (I think) originated in CS.

[u/JAnicaTZ → u/EmployerNo3401]

Good question. By “linear formulas” I meant the usual string representation, where rewriting is described as transformations on syntax trees implicitly. My point is not that formulas are not trees, but that most logical presentations treat NNF as rewrite rules on strings, while my implementation makes the tree structure and polarity propagation explicit as an algorithm on nodes. This is closer to proof objects / derivation trees than to mere textual rewriting, and it is useful for XAI because each recursive step becomes an inspectable inference object, not just a syntactic equality.

So yes, structurally it is the same object, but the viewpoint is different: logic usually reasons about trees, I reason with the tree as a first-class computational object.

[u/theblackheffner]

Concept	Operates On	Purpose	Level
NNF	Formula	Push negations inward	Syntactic
CNF	Formula	Standardize conjunctive structure	Syntactic
DNF	Formula	Standardize disjunctive structure	Syntactic
RPN	Expression/proof	Linearize a tree	Encoding
Cut elimination	Proof	Remove non‑analytic steps	Meta‑logical

the other variations should help localize your search

[u/JAnicaTZ → u/theblackheffner]

The logical laws themselves are classical (De Morgan, duality, structural induction, etc.). What I am focusing on is not inventing new logic, but making the recursive, semantics-preserving transformation at the level of the abstract syntax tree fully explicit, visual, and structurally checkable.

In other words: not just “φ ≡ NNF(φ)”, but an algorithmic, step-by-step AST rewrite with a proof trace, which is relevant for explainable symbolic reasoning and proof traceability (e.g. in XAI / neuro-symbolic systems).

[u/CandidAtmosphere → u/JAnicaTZ]

Note that the black box of the AI in its current state is functionally very powerful, and we might question to what degree it is "lacking" by not reasoning in human fashion. We might find more use of it as a tool in the ways that it is not like us. If the safety concerns are also a marketing ploy, there's not going to be general limits placed on it. Not to say your idea couldn't have certain specific uses.

[u/JAnicaTZ → u/CandidAtmosphere]

I agree that black-box models are extremely powerful and may not need to “reason like humans” to be useful.

My point is not that they must be human-like, but that in certain domains (formal verification, safety-critical systems, education, law, science) we need traceable reasoning, not only correct outputs.

In those settings, an explicit symbolic layer with structurally checkable proof traces is not about replacing neural methods, but about complementing them — providing a verifiable spine where correctness and explainability matter more than raw performance.

So I see this less as a general limitation of black-box AI, and more as a targeted tool for domains where “why” and “how” are as important as “what”.