ConjunctiveNormalForm

Conjunctive Normal Form (CNF) is a specific way of representing logical formulas. In conjunctive normal form, a logical formula is expressed as a conjunction (AND) of clauses, where each clause is a disjunction (OR) of one or more literals. A literal can be either an atomic proposition or its negation. The conjunctive normal form is often used in various algorithms and tools for solving logical problems because its properties are such that it is condicive to providing answering questions and affirming their well-posedness in an inference-theoretical way.