**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Concept# Negation normal form

Summary

In mathematical logic, a formula is in negation normal form (NNF) if the negation operator (\lnot, ) is only applied to variables and the only other allowed Boolean operators are conjunction (\land, ) and disjunction (\lor, ).
Negation normal form is not a canonical form: for example, a \land (b\lor \lnot c) and (a \land b) \lor (a \land \lnot c) are equivalent, and are both in negation normal form.
In classical logic and many modal logics, every formula can be brought into this form by replacing implications and equivalences by their definitions, using De Morgan's laws to push negation inwards, and eliminating double negations. This process can be represented using the following rewrite rules (Handbook of Automated Reasoning 1, p. 204):
:\begin{align}
A \Rightarrow B &~\to~ \lnot A \lor B \
A \Leftrightarrow B &~\to~ (\lnot A \lor B) \land (A \lor \lnot B) \
\lnot (A \lor B) &~\to~ \lnot A \land \

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications (1)

Related people

Related units

No results

No results

Loading

Related concepts (2)

Boolean function

In mathematics, a Boolean function is a function whose arguments and result assume values from a two-element set (usually {true, false}, {0,1} or {-1,1}). Alternative names are switching function, us

Boolean algebra

In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values true and false,

Related courses (2)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

EE-110: Logic systems (for MT)

Ce cours couvre les fondements des systèmes numériques. Sur la base d'algèbre Booléenne et de circuitscombinatoires et séquentiels incluant les machines d'états finis, les methodes d'analyse et de synthèse de systèmelogiques sont étudiées et appliquée

This thesis presents NC(T), an extension of the DPLL(T) scheme [16, 29] for decision procedures for quantifier-free first-order logics. In DPLL(T), a general Boolean DPLL engine is instantiated with a theory solver for the theory T. The DPLL engine is responsible for computing Boolean implications and detecting Boolean conflicts, while the theory solver detects implications and conflicts in T, and the communication between the two parts is done through a standardized interface. The Boolean reasoning is done on a set of constraints represented as clauses, meaning that formulas have to be converted to conjunctive normal form before they can be processed. The process results in the addition of variables and a general loss of structure. NC(T) remove this constraint by extending the Boolean engine to support the detection of implications and conflicts on non–clausal constraints, using techniques working on graphical representations of formulas in negation normal form first described in [19, 21]. Conversion to negation normal form preserves the size and structure of the input formula and does not introduce new variables. The above scheme NC(T) has been implemented as a tool called fstp, where the theory T under consideration is the quantifier–free theory of uninterpreted function and predicate symbols with equality. We describe our implementation and give early experimental results.

2008Related lectures (3)