Conjunctive normal form | EPFL Graph Search

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory. All conjunctions of literals and all disjunctions of literals are in CNF, as they can be seen as conjunctions of one-literal clauses and conjunctions of a single clause, respectively. As in the disjunctive normal form (DNF), the only propositional connectives a formula in CNF can contain are and, or, and not. The not operator can only be used as part of a literal, which means that it can only precede a propositional variable or a predicate symbol. In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals. All of the following formulas in the variables , and are in conjunctive normal form: For clarity, the disjunctive clauses are written inside parentheses above. In disjunctive normal form with parenthesized conjunctive clauses, the last case is the same, but the next to last is . The constants true and false are denoted by the empty conjunct and one clause consisting of the empty disjunct, but are normally written explicitly. The following formulas are not in conjunctive normal form: since an OR is nested within a NOT since an AND is nested within an OR Every formula can be equivalently written as a formula in conjunctive normal form. The three non-examples in CNF are: Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law. Since all propositional formulas can be converted into an equivalent formula in conjunctive normal form, proofs are often based on the assumption that all formulae are CNF.

Non-normal forms

Yves-Marie François Ducimetière

In this thesis, we propose to formally derive amplitude equations governing the weakly nonlinear evolution of non-normal dynamical systems, when they respond to harmonic or stochastic forcing, or to an initial condition. This approach reconciles the non-mo ...

EPFL2024

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...