Since it appears you can have arbitrarily deeply nested conjunctions and disjunctions (see this question), such as:
$$(((A ∧ B) ∨ (C ∧ (D ∨ E)) ∧ (F ∧ (G ∨ H)))$$
How do you "flatten" it, if you have the constraint that both conjunction and disjunction only have 2 arguments (that is they are binary operations)? That is, you are not allowed to do this:
$$(X ∨ Y) ∧ (W ∨ Z) ∧ (P ∨ Q) ∧ (S ∨ R)$$
That would really be:
$$((X ∨ Y) ∧ (W ∨ Z) ∧ (P ∨ Q) ∧ (S ∨ R))$$
And it would mean the disjunction takes an arbitrary amount of args (4 in this case).
So instead of flattening the list, like this, "into a conjunction of disjunctions", you would instead be forced to build a normalized tree of some sort (which I am not sure how that would look/work).
So given you must in the end have a tree instead of a flattened list (from a technical perspective), my question is how do you apply the transformation rules to get this tree like the first one into conjunctive normal form (CNF)? You don't have a "conjunction of disjunctions", as that is a flat list. Instead, you have a tree of disjunctions or something? Not quite sure what it should look like.
I am trying to figure out how to implement an algorithm for converting arbitrarily deeply nested propositional formulas into CNF. But I am stuck on the step of how to implement the conjunction and disjunction simplification functions (just those 2 functions). See Algorithm implementation to convert propositional formula into conjunctive normal form in JavaScript? for details.
Best Answer
In the usual official definitions of the syntax of propositional logic, conjunction and disjunction are binary operations. $A \land B \land C$ is just a short-hand for either of $(A \land B) \land C$ or $A \land (B \land C)$, Because $\land$ is associative, it doesn't matter which reading you take. (I think most people prefer $(A \land B) \land C$, because of the way they think of formulas like $x + y + z$ in arithmetic, but at least some computer scientists prefer the other reading.) For binary operations, like implication, that aren't associative, the brackets (or an agreed convention for inserting them) are a must and, again, there is some dispute about what the agreed convention should be.
For your implementation problem, you can design rewrite rules that move brackets to the right (say) and distribute disjunctions inside conjunctions to arrive at a CNF. You can then implement these rewrite rules either by hand-coding (along the lines of the partial solution in your link) or by implementing a general purpose rewrite function and providing a syntactic representation of the rewrite rules as a parameter. John Harrison's "Handbook of Practical Logic and Automated Reasoning" is a very good introduction to practical computational logic.