Conjunctive normal form (original) (raw)
Als konjunktive Normalform (kurz KNF, englisch CNF für conjunctive normal form) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet.
| Property | Value |
|---|---|
| dbo:abstract | 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 . (ca) 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. (cs) Als konjunktive Normalform (kurz KNF, englisch CNF für conjunctive normal form) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet. (de) 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. (en) 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. (es) 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). (fr) 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. (nl) 連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。 (ja) 불 대수에서 논리곱 표준형(conjunctive normal form)은 의 논리곱으로 나타낸 논리식을 말한다. 여기서 절은 의 논리합으로 이루어진다. 논리곱 표준형의 영문 표기를 줄여서 CNF라고도 한다. CNF와 반대로 리터럴의 논리곱으로 이루어진 절들을 논리합으로 연결할 수도 있다. 이를 이라고 한다. 모든 명제 논리식은 동등한 CNF로 변환될 수 있다. 이 변환은 이중부정 법칙, 드모르간 법칙, 분배 법칙 등을 써서 이루어진다. 리터럴의 개수가 3개 이하로 제한된 CNF를 3-CNF라고 하며 계산 이론에서 중요하게 다루어진다. 다른 개수로 제한할 때도 마찬가지로 정의할 수 있으나 2-CNF, 3-CNF 이외에는 중요하게 다루지 않는다. (ko) 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ń: (pl) 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. (it) 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 . (pt) Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ. Для этого можно использовать: закон двойного отрицания, закон де Моргана, дистрибутивность. (ru) Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції. (uk) 在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的。 所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和析取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。 例如，下列所有公式都是 CNF: 而下列不是: 上述三个公式分别等价于合取范式的下列三个公式: 所有命题公式都可以转换成 CNF 的等价公式。这种变换基于了关于逻辑等价的规则: 双重否定律、德·摩根定律和分配律。 因为所有逻辑公式都可以转换成合取范式的等价公式，证明经常基于所有公式都是 CNF 的假定。但是在某些情况下，这种到 CNF 的转换可能导致公式的指数性爆涨。例如，把下述非-CNF 公式转换成 CNF 生成有 个子句的公式: (zh) |
| dbo:wikiPageExternalLink | http://www.decision-procedures.org/handouts/Tseitin70.pdf https://www.mathematik.uni-marburg.de/~thormae/lectures/ti1/code/normalform/index.html https://archive.today/20121208184549/http:/www.izyt.com/BooleanLogic/applet.php https://books.google.com/books%3Fid=20Un1T78GlMC&q=%22conjunctive+normal+form%22%7Cdate=24 https://books.google.com/books%3Fid=3oJE9yczr3EC&q=%22conjunctive+normal+form%22%7Cdate=28 http://homepages.inf.ed.ac.uk/pbj/papers/sat04-bc-conv.pdf |
| dbo:wikiPageID | 73342 (xsd:integer) |
| dbo:wikiPageLength | 20930 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1097076255 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Canonical_normal_form dbr:Propositional_formula dbr:Quine–McCluskey_algorithm dbr:Model_theory dbr:Negation_normal_form dbr:Algebraic_normal_form dbc:Normal_forms_(logic) dbr:Resolution_(logic) dbr:De_Morgan's_laws dbr:Interpretation_(logic) dbr:Clausal_normal_form dbr:Skolem_normal_form dbr:NP-complete dbr:NP-hard dbr:Equisatisfiability dbr:Redex dbr:Logical_conjunction dbr:Clause_(logic) dbr:Computational_complexity_theory dbr:Horn_clause dbr:Automated_theorem_proving dbr:First-order_logic dbr:Logical_disjunction dbr:Logical_equivalence dbr:2-satisfiability dbr:Disjunctive_normal_form dbr:Double_negation_elimination dbr:Boolean_algebra dbr:Boolean_satisfiability_problem dbr:Circuit_theory dbr:Polynomial_time dbr:Literal_(mathematical_logic) dbr:Propositional_variable dbr:Boolean_logic dbr:Satisfiability_and_validity dbr:Tseitin_transformation dbr:Distributive_law dbr:Formula_(mathematical_logic) dbr:De_Morgan's_Law dbr:Logical_negation |
| dbp:id | p/c025090 (en) |
| dbp:title | Conjunctive normal form (en) |
| dbp:wikiPageUsesTemplate | dbt:Springer dbt:Cite_book dbt:Distinguish dbt:Mvar dbt:Short_description |
| dcterms:subject | dbc:Normal_forms_(logic) |
| gold:hypernym | dbr:Conjunction |
| rdf:type | owl:Thing dbo:Building |
| rdfs:comment | Als konjunktive Normalform (kurz KNF, englisch CNF für conjunctive normal form) wird in der Aussagenlogik eine bestimmte Form von Formeln bezeichnet. (de) 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). (fr) 連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。 (ja) 불 대수에서 논리곱 표준형(conjunctive normal form)은 의 논리곱으로 나타낸 논리식을 말한다. 여기서 절은 의 논리합으로 이루어진다. 논리곱 표준형의 영문 표기를 줄여서 CNF라고도 한다. CNF와 반대로 리터럴의 논리곱으로 이루어진 절들을 논리합으로 연결할 수도 있다. 이를 이라고 한다. 모든 명제 논리식은 동등한 CNF로 변환될 수 있다. 이 변환은 이중부정 법칙, 드모르간 법칙, 분배 법칙 등을 써서 이루어진다. 리터럴의 개수가 3개 이하로 제한된 CNF를 3-CNF라고 하며 계산 이론에서 중요하게 다루어진다. 다른 개수로 제한할 때도 마찬가지로 정의할 수 있으나 2-CNF, 3-CNF 이외에는 중요하게 다루지 않는다. (ko) 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ń: (pl) Конъюнкти́вная норма́льная фо́рма (КНФ) в булевой логике — нормальная форма, в которой булева формула имеет вид конъюнкции дизъюнкций литералов. Конъюнктивная нормальная форма удобна для автоматического доказательства теорем. Любая булева формула может быть приведена к КНФ. Для этого можно использовать: закон двойного отрицания, закон де Моргана, дистрибутивность. (ru) Кон'юнкти́вна норма́льна фо́рма (КНФ) в булевій логіці - нормальна форма в якій булева формула має вид кон'юнкції декількох диз'юнктів (де диз'юнктами називаються диз'юнкції декількох пропозиційних символів або їх заперечень). Кон'юнктивна нормальна форма широко використовується в автоматичному доведенні теорем, зокрема вона є основою для використання правила резолюції. (uk) 在布尔逻辑中，如果一个公式是子句的合取，那么它是合取范式(CNF)的。作为规范形式，它在自动定理证明中有用。它类似于在电路理论中的。 所有的文字的合取和所有的文字的析取是 CNF 的，因为可以被分别看作一个文字的子句的合取和析取。和析取范式(DNF)中一样，在 CNF 公式中可以包含的命题连结词是与、或和非。非算子只能用做文字的一部分，这意味着它只能在命题变量前出现。 例如，下列所有公式都是 CNF: 而下列不是: 上述三个公式分别等价于合取范式的下列三个公式: 所有命题公式都可以转换成 CNF 的等价公式。这种变换基于了关于逻辑等价的规则: 双重否定律、德·摩根定律和分配律。 因为所有逻辑公式都可以转换成合取范式的等价公式，证明经常基于所有公式都是 CNF 的假定。但是在某些情况下，这种到 CNF 的转换可能导致公式的指数性爆涨。例如，把下述非-CNF 公式转换成 CNF 生成有 个子句的公式: (zh) 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. (ca) 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. (cs) 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. (en) 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. (es) 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. (it) 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. (nl) 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. (pt) |
| rdfs:label | Conjunctive normal form (en) Forma normal conjuntiva (ca) Konjunktivní normální forma (cs) Konjunktive Normalform (de) Forma normal conjuntiva (es) Forme normale conjonctive (fr) Forma normale congiuntiva (it) 논리곱 표준형 (ko) 連言標準形 (ja) Conjunctieve normaalvorm (nl) Koniunkcyjna postać normalna (pl) Forma normal conjuntiva (pt) Конъюнктивная нормальная форма (ru) Кон'юнктивна нормальна форма (uk) 合取范式 (zh) |
| owl:differentFrom | dbr:Chomsky_normal_form |
| owl:sameAs | freebase:Conjunctive normal form wikidata:Conjunctive normal form dbpedia-ca:Conjunctive normal form dbpedia-cs:Conjunctive normal form dbpedia-de:Conjunctive normal form dbpedia-es:Conjunctive normal form dbpedia-fa:Conjunctive normal form dbpedia-fr:Conjunctive normal form dbpedia-he:Conjunctive normal form dbpedia-hu:Conjunctive normal form http://hy.dbpedia.org/resource/Կոնյունկտիվ_նորմալ_ձև dbpedia-it:Conjunctive normal form dbpedia-ja:Conjunctive normal form dbpedia-ko:Conjunctive normal form dbpedia-nl:Conjunctive normal form dbpedia-pl:Conjunctive normal form dbpedia-pt:Conjunctive normal form dbpedia-ru:Conjunctive normal form dbpedia-sh:Conjunctive normal form dbpedia-sr:Conjunctive normal form dbpedia-uk:Conjunctive normal form dbpedia-zh:Conjunctive normal form https://global.dbpedia.org/id/51MNy |
| prov:wasDerivedFrom | wikipedia-en:Conjunctive_normal_form?oldid=1097076255&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Conjunctive_normal_form |
| is dbo:wikiPageDisambiguates of | dbr:Normal_form dbr:CNF |
| is dbo:wikiPageRedirects of | dbr:Clausal_normal_form dbr:Product-of-sums_expression dbr:Conjunctive_Normal_Form dbr:Conjunctive_normal_formula dbr:Clausal_form dbr:Clause_normal_form dbr:3-CNF |
| is dbo:wikiPageWikiLink of | dbr:Canonical_normal_form dbr:Propositional_formula dbr:Entropy_compression dbr:Enumeration_algorithm dbr:List_of_algorithms dbr:Negation_normal_form dbr:Parsimonious_reduction dbr:Bayesian_network dbr:Algebraic_normal_form dbr:Algorithm_selection dbr:Algorithmic_Lovász_local_lemma dbr:Resolution_(logic) dbr:DPLL_algorithm dbr:Vampire_(theorem_prover) dbr:De_Morgan's_laws dbr:Decision_list dbr:E_(theorem_prover) dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(A–C) dbr:♯P dbr:♯P-completeness_of_01-permanent dbr:(SAT,_ε-UNSAT) dbr:Corresponding_conditional dbr:Craig_interpolation dbr:Median_graph dbr:Generalized_geography dbr:Clausal_normal_form dbr:NOR_logic dbr:Normal_form dbr:Prenex_normal_form dbr:Rewriting dbr:Clique_problem dbr:Conflict-driven_clause_learning dbr:Cook–Levin_theorem dbr:Equisatisfiability dbr:Vocabulary_mismatch dbr:Product-of-sums_expression dbr:MAXEkSAT dbr:Skew-symmetric_graph dbr:Clause_(logic) dbr:Feature_model dbr:Parity_function dbr:Maker-Breaker_game dbr:Max/min_CSP/Ones_classification_theorems dbr:Maximum_satisfiability_problem dbr:Occurs_check dbr:Time_complexity dbr:Karp's_21_NP-complete_problems dbr:Laws_of_Form dbr:List_of_Boolean_algebra_topics dbr:Local_search_(constraint_satisfaction) dbr:Causal_map dbr:Knowledge_compilation dbr:2-satisfiability dbr:Harry_R._Lewis dbr:Jean_Gallier dbr:Tautology_(logic) dbr:Cox's_theorem dbr:Unsatisfiable_core dbr:APX dbr:Hex_(board_game) dbr:Holographic_algorithm dbr:Disjunctive_normal_form dbr:Artificial_neuron dbr:Boolean_function dbr:Boolean_satisfiability_algorithm_heuristics dbr:Boolean_satisfiability_problem dbr:Circuit_satisfiability_problem dbr:Conjunctive_Normal_Form dbr:Conjunctive_normal_formula dbr:Canonical_form dbr:Read-once_function dbr:CNF dbr:SAT_solver dbr:SNP_(complexity) dbr:Sharp-SAT dbr:Exponential_time_hypothesis dbr:Implication_graph dbr:Literal_(mathematical_logic) dbr:NP-intermediate dbr:NL-complete dbr:Switching_lemma dbr:Tseytin_transformation dbr:WalkSAT dbr:True_quantified_Boolean_formula dbr:Clausal_form dbr:Clause_normal_form dbr:3-CNF |
| is owl:differentFrom of | dbr:Chomsky_normal_form |
| is foaf:primaryTopic of | wikipedia-en:Conjunctive_normal_form |