This HTML5 document contains 131 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dbt	http://dbpedia.org/resource/Template:
wikipedia-en	http://en.wikipedia.org/wiki/
n12	http://hy.dbpedia.org/resource/
dbr	http://dbpedia.org/resource/
dbpedia-sh	http://sh.dbpedia.org/resource/
dbpedia-he	http://he.dbpedia.org/resource/
dbpedia-fr	http://fr.dbpedia.org/resource/
n38	https://archive.today/20121208184549/http:/www.izyt.com/BooleanLogic/
n10	http://www.decision-procedures.org/handouts/
dcterms	http://purl.org/dc/terms/
rdfs	http://www.w3.org/2000/01/rdf-schema#
dbpedia-cs	http://cs.dbpedia.org/resource/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
dbp	http://dbpedia.org/property/
n34	https://www.mathematik.uni-marburg.de/~thormae/lectures/ti1/code/normalform/
xsdh	http://www.w3.org/2001/XMLSchema#
dbpedia-uk	http://uk.dbpedia.org/resource/
dbo	http://dbpedia.org/ontology/
dbpedia-sr	http://sr.dbpedia.org/resource/
n14	https://books.google.com/
dbpedia-pt	http://pt.dbpedia.org/resource/
dbpedia-hu	http://hu.dbpedia.org/resource/
dbpedia-ja	http://ja.dbpedia.org/resource/
dbc	http://dbpedia.org/resource/Category:
dbpedia-de	http://de.dbpedia.org/resource/
dbpedia-pl	http://pl.dbpedia.org/resource/
dbpedia-ru	http://ru.dbpedia.org/resource/
wikidata	http://www.wikidata.org/entity/
gold	http://purl.org/linguistics/gold/
dbpedia-nl	http://nl.dbpedia.org/resource/
n36	https://global.dbpedia.org/id/
n7	http://homepages.inf.ed.ac.uk/pbj/papers/
dbpedia-it	http://it.dbpedia.org/resource/
dbpedia-ca	http://ca.dbpedia.org/resource/
prov	http://www.w3.org/ns/prov#
foaf	http://xmlns.com/foaf/0.1/
dbpedia-zh	http://zh.dbpedia.org/resource/
dbpedia-ko	http://ko.dbpedia.org/resource/
dbpedia-fa	http://fa.dbpedia.org/resource/
dbpedia-es	http://es.dbpedia.org/resource/
freebase	http://rdf.freebase.com/ns/
owl	http://www.w3.org/2002/07/owl#

Statements

Subject Item

dbr:Conjunctive_normal_form

rdf:type

owl:Thing dbo:Building

rdfs:label

Conjunctive normal form 合取范式 Конъюнктивная нормальная форма Кон'юнктивна нормальна форма Forma normal conjuntiva 連言標準形 Forme normale conjonctive Konjunktivní normální forma Koniunkcyjna postać normalna Forma normale congiuntiva Forma normal conjuntiva Conjunctieve normaalvorm 논리곱 표준형 Forma normal conjuntiva Konjunktive Normalform

rdfs:comment

En lògica booleana, una fórmula està en forma normal conjuntiva (FNC) si correspon a una conjunció de clàusules, on una clàusula és una disjunció de , on un literal i el seu complement no poden aparèixer en la mateixa clàusula. Aquesta definició és similar a la de emprades en teoria de circuits. Na lógica booleana, uma fórmula está na forma normal conjuntiva (FNC) se é uma conjunção de cláusulas, onde uma cláusula é uma disjunção de literais. Sendo uma forma normal, a FNC é útil em . Ela é similar à usada na teoria dos circuitos. Por exemplo, todas as fórmulas seguintes estão na FNC: : Porém, as seguintes fórmulas não estão: As três fórmulas acima são equivalentes respectivamente às três fórmulas seguintes que estão na forma normal conjuntiva: A seguinte fórmula é uma gramática formal para FNC: 1. → ∨2. → ∧3. → ¬4. → 5. → 6. → 7. →8. → 9. → Onde é qualquer variável. 불 대수에서 논리곱 표준형(conjunctive normal form)은 의 논리곱으로 나타낸 논리식을 말한다. 여기서 절은 의 논리합으로 이루어진다. 논리곱 표준형의 영문 표기를 줄여서 CNF라고도 한다. CNF와 반대로 리터럴의 논리곱으로 이루어진 절들을 논리합으로 연결할 수도 있다. 이를 이라고 한다. 모든 명제 논리식은 동등한 CNF로 변환될 수 있다. 이 변환은 이중부정 법칙, 드모르간 법칙, 분배 법칙 등을 써서 이루어진다. 리터럴의 개수가 3개 이하로 제한된 CNF를 3-CNF라고 하며 계산 이론에서 중요하게 다루어진다. 다른 개수로 제한할 때도 마찬가지로 정의할 수 있으나 2-CNF, 3-CNF 이외에는 중요하게 다루지 않는다. 在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的。 所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和析取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。 例如，下列所有公式都是 CNF: 而下列不是: 上述三个公式分别等价于合取范式的下列三个公式: 所有命题公式都可以转换成 CNF 的等价公式。这种变换基于了关于逻辑等价的规则: 双重否定律、德·摩根定律和分配律。 因为所有逻辑公式都可以转换成合取范式的等价公式，证明经常基于所有公式都是 CNF 的假定。但是在某些情况下，这种到 CNF 的转换可能导致公式的指数性爆涨。例如，把下述非-CNF 公式转换成 CNF 生成有 个子句的公式: Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції. Als konjunktive Normalform (kurz KNF, englisch CNF für conjunctive normal form) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet. Nella logica booleana, una formula è in forma normale congiuntiva o congiunta (FNC), indicata anche come CNF (acronimo di Conjunctive Normal Form) se è una congiunzione di clausole, dove le clausole sono una disgiunzione di letterali. Una formula in CNF ha quindi la seguente struttura: : Numero di clausole. : Numero di letterali della clausola i-esima. : È il k-esimo letterale della i-esima clausola. Un letterale può essere una variabile booleana (cioè che può valere solo 0 o 1, vero o falso) o la negazione di una variabile. En lógica booleana, una fórmula está en forma normal conjuntiva (FNC) si corresponde a una conjunción de cláusulas, donde una cláusula es una disyunción de literales, donde un literal y su complemento no pueden aparecer en la misma cláusula. Esta definición es similar a la de forma de productos de sumas usadas en teoría de circuitos. En demostración automática de teoremas, la noción de «forma normal clausal» se utiliza frecuentemente en un sentido más estricto, significando una representación particular de una fórmula FNC como un conjunto de conjuntos de literales. Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ. Для этого можно использовать: закон двойного отрицания, закон де Моргана, дистрибутивность. 連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。 In de logica is een formule in conjunctieve normaalvorm (Eng. conjunctive normal form, CNF, ook wel afgekort als CNV) als die bestaat uit een conjunctie van disjuncties met literalen (ook een conjunctie van clausules genoemd). In een conjunctieve normaalvorm komen alleen de booleaanse operatoren 'en', 'of' en negatie voor, waarbij de negatie alleen als onderdeel van een literaal kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties. En logique booléenne et en calcul des propositions, une formule en forme normale conjonctive ou FNC (en anglais, Conjunctive Normal Form, Clausal Normal Form ou CNF) est une conjonction de clauses, où une clause est une disjonction de littéraux. Les formules en FNC sont utilisées dans le cadre de la démonstration automatique de théorèmes ou encore dans la résolution du problème SAT (en particulier dans l'algorithme DPLL). Vevýrokové logice je formule v konjunktivní normální formě (KNF nebo CNF z anglického conjunctive normal form), pokud je ve tvaru konjunkcí , kde klauzuli definujeme jako disjunkci (a je-li výroková proměnná, tak jí určené literály jsou právě a ). Jako normální forma se používá v . Podobná kanonická forma se používá v teorii obvodů. Platí, že pro každou formuli A lze sestrojit ekvivalentní formule K a D (tedy A ↔ K a A ↔ D), kde K je v KNF a D je v DNF. Toto tvrzení lze dokázat indukcí podle složitosti formule užitím De Morganových zákonů a distributivity. Koniunkcyjna postać normalna (ang. conjunctive normal form, CNF) danej formuły logicznej to równoważna jej formuła zapisana w postaci koniunkcji klauzul. Na przykład koniunkcyjną postacią normalną wyrażenia jest Każde wyrażenie logiczne ma koniunkcyjną postać normalną. Przykłady przekształceń: 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. 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.

owl:differentFrom

dbr:Chomsky_normal_form

dcterms:subject

dbc:Normal_forms_(logic)

dbo:wikiPageID

73342

dbo:wikiPageRevisionID

1097076255

dbo:wikiPageWikiLink

dbr:Satisfiability_and_validity dbr:De_Morgan's_laws dbr:Horn_clause dbr:De_Morgan's_Law dbr:Tseitin_transformation dbr:Circuit_theory dbr:First-order_logic dbr:Redex dbr:Boolean_logic dbr:Computational_complexity_theory dbr:Formula_(mathematical_logic) dbr:Double_negation_elimination dbr:Interpretation_(logic) dbr:2-satisfiability dbr:NP-complete dbr:NP-hard dbr:Automated_theorem_proving dbr:Boolean_satisfiability_problem dbr:Propositional_formula dbr:Polynomial_time dbr:Quine–McCluskey_algorithm dbr:Equisatisfiability dbr:Logical_equivalence dbc:Normal_forms_(logic) dbr:Distributive_law dbr:Algebraic_normal_form dbr:Disjunctive_normal_form dbr:Literal_(mathematical_logic) dbr:Resolution_(logic) dbr:Skolem_normal_form dbr:Clause_(logic) dbr:Logical_negation dbr:Negation_normal_form dbr:Model_theory dbr:Logical_disjunction dbr:Propositional_variable dbr:Canonical_normal_form dbr:Logical_conjunction dbr:Boolean_algebra dbr:Clausal_normal_form

dbo:wikiPageExternalLink

n7:sat04-bc-conv.pdf n10:Tseitin70.pdf n14:books%3Fid=20Un1T78GlMC&q=%22conjunctive+normal+form%22%7Cdate=24 n14:books%3Fid=3oJE9yczr3EC&q=%22conjunctive+normal+form%22%7Cdate=28 n34:index.html n38:applet.php

owl:sameAs

dbpedia-zh:合取范式 dbpedia-hu:Konjunktív_normálforma n12:Կոնյունկտիվ_նորմալ_ձև dbpedia-pl:Koniunkcyjna_postać_normalna dbpedia-ja:連言標準形 dbpedia-cs:Konjunktivní_normální_forma dbpedia-pt:Forma_normal_conjuntiva dbpedia-de:Konjunktive_Normalform dbpedia-sh:Konjuktivna_normalna_forma dbpedia-fa:فرم_نرمال_اشتراکی dbpedia-ru:Конъюнктивная_нормальная_форма dbpedia-nl:Conjunctieve_normaalvorm dbpedia-ko:논리곱_표준형 wikidata:Q846564 freebase:m.0jpxc dbpedia-sr:Конјунктивна_нормална_форма dbpedia-he:CNF dbpedia-ca:Forma_normal_conjuntiva n36:51MNy dbpedia-it:Forma_normale_congiuntiva dbpedia-uk:Кон'юнктивна_нормальна_форма dbpedia-es:Forma_normal_conjuntiva dbpedia-fr:Forme_normale_conjonctive

dbp:wikiPageUsesTemplate

dbt:Springer dbt:Mvar dbt:Short_description dbt:Cite_book dbt:Distinguish

dbp:id

p/c025090

dbp:title

Conjunctive normal form

dbo:abstract

En lógica booleana, una fórmula está en forma normal conjuntiva (FNC) si corresponde a una conjunción de cláusulas, donde una cláusula es una disyunción de literales, donde un literal y su complemento no pueden aparecer en la misma cláusula. Esta definición es similar a la de forma de productos de sumas usadas en teoría de circuitos. Todas las conjunciones de literales y todas las disyunciones de literales están en FNC, puesto que pueden ser vistas, respectivamente, como conjunciones de cláusulas de un literal, y como conjunciones de una única cláusula. Al igual que en una forma normal disyuntiva (FND), los únicos conectivos lógicos que pueden aparecer en una fórmula en FNC son la conjunción, disyunción y negación. El operador negación solo puede aplicarse a un literal, y no a una cláusula completa, lo que significa que este sólo puede preceder a una variable proposicional o un símbolo de predicado. En demostración automática de teoremas, la noción de «forma normal clausal» se utiliza frecuentemente en un sentido más estricto, significando una representación particular de una fórmula FNC como un conjunto de conjuntos de literales. En lògica booleana, una fórmula està en forma normal conjuntiva (FNC) si correspon a una conjunció de clàusules, on una clàusula és una disjunció de , on un literal i el seu complement no poden aparèixer en la mateixa clàusula. Aquesta definició és similar a la de emprades en teoria de circuits. Totes les conjuncions de literals i totes les disjuncions de literals estan en FNC, car poden ser vistes, respectivament, com a conjuncions de clàusules d'un literal, i com a conjuncions d'una única clàusula. De la mateixa manera que en forma normal disjuntiva (FND), els únics connectors lògics que poden aparèixer en una fórmula en FNC són la conjunció, la disjunció i la negació. L'operador negació només pot aplicar-se a un literal, i no a una clàusula completa, la qual cosa significa que només pot precedir una . Vevýrokové logice je formule v konjunktivní normální formě (KNF nebo CNF z anglického conjunctive normal form), pokud je ve tvaru konjunkcí , kde klauzuli definujeme jako disjunkci (a je-li výroková proměnná, tak jí určené literály jsou právě a ). Jako normální forma se používá v . Podobná kanonická forma se používá v teorii obvodů. Každá konjunkce literálů a také každá disjunkce literálů je KNF, protože je můžeme považovat za konjunkci klauzulí s jedním literálem, resp. za disjunkci jedné klauzule.Podobně jako vdisjunktivní normální formě (DNF), jediné logické spojky v KNF jsou logická spojka a, nebo a negace. Negace může být pouze součástí literálu, tzn. že negovat lze pouze výrokovou proměnnou. Platí, že pro každou formuli A lze sestrojit ekvivalentní formule K a D (tedy A ↔ K a A ↔ D), kde K je v KNF a D je v DNF. Toto tvrzení lze dokázat indukcí podle složitosti formule užitím De Morganových zákonů a distributivity. Koniunkcyjna postać normalna (ang. conjunctive normal form, CNF) danej formuły logicznej to równoważna jej formuła zapisana w postaci koniunkcji klauzul. Na przykład koniunkcyjną postacią normalną wyrażenia jest Każde wyrażenie logiczne ma koniunkcyjną postać normalną. Przykłady przekształceń: 連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。 Na lógica booleana, uma fórmula está na forma normal conjuntiva (FNC) se é uma conjunção de cláusulas, onde uma cláusula é uma disjunção de literais. Sendo uma forma normal, a FNC é útil em . Ela é similar à usada na teoria dos circuitos. Toda conjunção de literais e toda disjunção de literais estão na FNC, já que elas podem ser vistas como conjunções de cláusulas de um literal e conjunções de uma só cláusula, respectivamente. Assim como na forma normal disjuntiva (FND), os únicos conectivos proposicionais que uma fórmula na FNC pode conter são os operadores e, ou e não. O operador não pode ser usado apenas como parte de um literal, e portanto ele pode aparecer apenas na frente de . Por exemplo, todas as fórmulas seguintes estão na FNC: : Porém, as seguintes fórmulas não estão: As três fórmulas acima são equivalentes respectivamente às três fórmulas seguintes que estão na forma normal conjuntiva: Toda fórmula proposicional pode ser convertida para uma fórmula equivalente que está na FNC.Essa transformação é baseada em regras sobre : Lei da Dupla Negação, Leis de De Morgan, e a Distributividade. Uma vez que todas as fórmulas lógicas clássicas podem ser convertidas em fórmulas equivalentes na forma normal conjuntiva, muitas demonstrações são baseadas na suposição de que todas as fórmulas estão na FNC. Contudo, em alguns casos, essa conversão para FNC pode levar a uma explosão exponencial da fórmula. Por exemplo, traduzindo a seguinte fórmula que não está na FNC para FNC, obtemos uma fórmula com cláusulas: A seguinte fórmula é uma gramática formal para FNC: 1. → ∨2. → ∧3. → ¬4. → 5. → 6. → 7. →8. → 9. → Onde é qualquer variável. Existem transformações das fórmulas na FNC que preservam a satisfatibilidade ao invés da equivalência e não produzem um aumento exponencial do tamanho. Tais transformações aumentam o tamanho da fórmula apenas por um fator linear, mas introduzem novas variáveis. A forma normal conjuntiva pode ser levada adiante de modo a produzir a forma normal clausal de uma fórmula lógica, a qual é usada para se efetuar resolução de primeira ordem. Um importante conjunto de problemas em complexidade computacional envolve encontrar atribuições para as variáveis de uma fórmula booleana expressa na Forma Normal Conjuntiva, tais que a fórmula seja satisfeita. O problema k-SAT é o problema de encontrar uma atribuição que satisfaça para uma fórmula booleana expressa na FNC, tal que cada disjunção contenha no máximo k variáveis. 3-SAT é NP-completo (assim como qualquer outro problema k-SAT com k>2), enquanto pode ser resolvido em . Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ. Для этого можно использовать: закон двойного отрицания, закон де Моргана, дистрибутивность. En logique booléenne et en calcul des propositions, une formule en forme normale conjonctive ou FNC (en anglais, Conjunctive Normal Form, Clausal Normal Form ou CNF) est une conjonction de clauses, où une clause est une disjonction de littéraux. Les formules en FNC sont utilisées dans le cadre de la démonstration automatique de théorèmes ou encore dans la résolution du problème SAT (en particulier dans l'algorithme DPLL). Als konjunktive Normalform (kurz KNF, englisch CNF für conjunctive normal form) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet. In de logica is een formule in conjunctieve normaalvorm (Eng. conjunctive normal form, CNF, ook wel afgekort als CNV) als die bestaat uit een conjunctie van disjuncties met literalen (ook een conjunctie van clausules genoemd). In een conjunctieve normaalvorm komen alleen de booleaanse operatoren 'en', 'of' en negatie voor, waarbij de negatie alleen als onderdeel van een literaal kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties. Elke formule kan omgezet worden naar een equivalente formule in conjunctieve normaalvorm met behulp van equivalentieregels (zoals de wetten van De Morgan en distributiviteit) die de formule omschrijven naar een logisch equivalente vorm in CNF. 불 대수에서 논리곱 표준형(conjunctive normal form)은 의 논리곱으로 나타낸 논리식을 말한다. 여기서 절은 의 논리합으로 이루어진다. 논리곱 표준형의 영문 표기를 줄여서 CNF라고도 한다. CNF와 반대로 리터럴의 논리곱으로 이루어진 절들을 논리합으로 연결할 수도 있다. 이를 이라고 한다. 모든 명제 논리식은 동등한 CNF로 변환될 수 있다. 이 변환은 이중부정 법칙, 드모르간 법칙, 분배 법칙 등을 써서 이루어진다. 리터럴의 개수가 3개 이하로 제한된 CNF를 3-CNF라고 하며 계산 이론에서 중요하게 다루어진다. 다른 개수로 제한할 때도 마찬가지로 정의할 수 있으나 2-CNF, 3-CNF 이외에는 중요하게 다루지 않는다. Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції. Nella logica booleana, una formula è in forma normale congiuntiva o congiunta (FNC), indicata anche come CNF (acronimo di Conjunctive Normal Form) se è una congiunzione di clausole, dove le clausole sono una disgiunzione di letterali. Una formula in CNF ha quindi la seguente struttura: : Numero di clausole. : Numero di letterali della clausola i-esima. : È il k-esimo letterale della i-esima clausola. Un letterale può essere una variabile booleana (cioè che può valere solo 0 o 1, vero o falso) o la negazione di una variabile. Una funzione booleana è una funzione che ha in ingresso diversi valori booleani (cioè vero/falso oppure 1/0) e come risultato ha un valore booleano. Per ogni funzione booleana, esiste una formula in forma normale congiuntiva che produce come risultato gli stessi valori. 在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的。 所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和析取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。 例如，下列所有公式都是 CNF: 而下列不是: 上述三个公式分别等价于合取范式的下列三个公式: 所有命题公式都可以转换成 CNF 的等价公式。这种变换基于了关于逻辑等价的规则: 双重否定律、德·摩根定律和分配律。 因为所有逻辑公式都可以转换成合取范式的等价公式，证明经常基于所有公式都是 CNF 的假定。但是在某些情况下，这种到 CNF 的转换可能导致公式的指数性爆涨。例如，把下述非-CNF 公式转换成 CNF 生成有 个子句的公式: 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.

gold:hypernym

dbr:Conjunction

prov:wasDerivedFrom

wikipedia-en:Conjunctive_normal_form?oldid=1097076255&ns=0

dbo:wikiPageLength

20930

foaf:isPrimaryTopicOf

wikipedia-en:Conjunctive_normal_form