Negation normal form

A logical formula is in negation normal form if negation occurs only immediately above elementary propositions, and {$\lnot, \lor,\land$} are the only allowed Boolean connectives. In classical logic each formula can be brought into this form by replacing implications and equivalences by their definitions, using De Morgan's laws to push negation inside, and eliminating double negations. This process can be represented using the following rewrite rules:

$\lnot (\forall x. G) \to \exists x. \lnot G$

$\lnot (\exists x. G) \to \forall x. \lnot G$

$\lnot \lnot G \to G$

$\lnot (G_1 \land G_2) \to (\lnot G_1) \lor (\lnot G_2)$

$\lnot (G_1 \lor G_2) \to (\lnot G_1) \land (\lnot G_2)$

A formula in negation normal form can be put into the stronger conjunctive normal form or disjunctive normal form by applying the distributivity laws.

External links

• Java applet for converting logical formula to Negation Normal Form, showing laws used

This logic-related article is a stub. You can help Wikipedia by expanding it.v · Categories: Propositional calculus Normal forms (logic) Logic stubs Wikimedia Foundation. 2010. Игры ⚽ Нужно решить контрольную? Henry Drummond St. Pepin (grape) Look at other dictionaries: Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… …   Wikipedia Conjunctive normal form — In Boolean logic, a formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals. As a normal form, it is useful in automated theorem proving. It is similar to the product of sums form …   Wikipedia Clausal normal form — The clausal normal form (or clause normal form, conjunctive normal form, CNF) of a logical formula is used in logic programming and many theorem proving systems. A formula in clause normal form is a set of clauses, interpreted as a conjunction. A …   Wikipedia Prenex normal form — A formula of the predicate calculus is in prenex[1] normal form if it is written as a string of quantifiers followed by a quantifier free part (referred to as the matrix). Every formula in classical logic is equivalent to a formula in prenex… …   Wikipedia Negational normal form — Negative normal form is way to represent the formula by keeping the negation symbol only to the literals. If α and φ are boolean formulas, then α φ , α φ, α, α φ are all boolean formulas. The boolean formulas are made up of literals which are… …   Wikipedia Canonical form — Generally, in mathematics, a canonical form (often called normal form or standard form) of an object is a standard way of presenting that object. Canonical form can also mean a differential form that is defined in a natural (canonical) way; see… …   Wikipedia Laws of Form — (hereinafter LoF ) is a book by G. Spencer Brown, published in 1969, that straddles the boundary between mathematics and of philosophy. LoF describes three distinct logical systems: * The primary arithmetic (described in Chapter 4), whose models… …   Wikipedia Caltech Intermediate Form — Infobox file format name = Caltech Intermediate Form(at) extension = .cif mime = owner = creatorcode = strubin genre = EDA file format containerfor = containedby = extendedfrom = extendedto = Caltech Intermediate Form (CIF) is a file format for… …   Wikipedia NNF — Negation Normal Form (Academic & Science » Mathematics) * Nuveen Insured New York Premium Income Fund (Business » NYSE Symbols) * Non Normal Form (Academic & Science » Mathematics) * New National Framework (Computing » Networking) * New National… …   Abbreviations dictionary Method of analytic tableaux — A graphical representation of a partially built propositional tableau In proof theory, the semantic tableau (or truth tree) is a decision procedure for sentential and related logics, and a proof procedure for formulas of first order logic. The… …   Wikipedia 18+ © Academic, 2000-2024 Contact us: Technical Support, Advertising Dictionaries export, created on PHP, Joomla, Drupal, WordPress, MODx. Mark and share Search through all dictionaries Translate… Search Internet Share the article and excerpts Direct link … Do a right-click on the link above and select “Copy Link”