| p:abstract
| - 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 clause is an implicitly universally quantified set of literals, interpreted as a disjunction. If variant clauses are identified, the clause normal form of a formula is unique. The procedure to convert a formula into clausal form can destroy the structure of the formula, and naive translations often causes exponential blowup in the size of the resulting formula. The procedure begins with any formula of classical first-order logic: Put the formula into negation normal form. Standardize variables <math> \vee </math> becomes <math> \vee </math>, where <math>c</math> is new Skolemize -- replace existential variables with Skolem constants or Skolem functions of universal variables, from the outside inward. Make the following replacements: <math>\forall x \exists y \, P</math> becomes <math>, \forall x \, P</math>, where <math>f_c</math> is new Remove the universal quantifiers. Put the formula into conjunctive normal form. Replace <math>C1 \wedge \cdots \wedge Cn</math> with <math>\{ C1, \dots, Cn \}</math>. Each conjunct is of the form <math>\neg A1 \vee \cdots \vee \neg Am \vee B1 \vee \cdots \vee Bn</math>, which is equivalent to <math> \to </math>. If m=0 and n=1, this is a Prolog fact. If m>0 and n=1, this is a Prolog rule. If m>0 and n=0, this is a Prolog query. Finally, replace each conjunct <math> \to </math> with <math>\{ A1 \wedge \cdots \wedge Am \to B1, A1 \wedge \cdots \wedge Am \to B2, \cdots, A1 \wedge \cdots \wedge Am \to Bn \}</math>. When n = 1, the logic is called Horn clause logic and is equivalent in computational power to a universal Turing machine. Often it is sufficient to generate an equisatisfiable (not an equivalent) CNF for a formula. In this case, the worst-case exponential blow-up can be avoided by introducing definitions and using them to rename parts of the formula. (en)
- 節標準形（英: Clausal normal form、CNF）とは、論理プログラミングや多くの自動定理証明系で使われる論理式の標準形式である。論理式を節標準形に変換すると論理式の構造が破壊され、単純な変換をすると式のサイズが指数関数的に増大することが多い。 (ja)
- A forma normal clausal é usada em programação lógica e em muitos sistemas provadores de teoremas. O procedimento de conversão de uma fórmula para a forma clausal pode destruir a estrutura da fórmula e, além disso, traduções feitas de forma descuidada freqüentemente causam o crescimento exponencial no tamanho da fórmula resultante. O procedimento começa com uma fórmula qualquer da lógica clássica de primeira ordem: Coloque a fórmula na forma normal prenex. Realize o fecho universal da fórmula. Skolemize - substitua as variáveis existenciais por constantes de Skolem ou funções de Skolem de variáveis universais, de fora para dentro. Faça as seguintes substituições: <math>\exists x. P</math> torna-se <math>P</math>, onde <math>c</math> é novo. <math>\forall x. ... \exists y. P</math> torna-se <math>\forall x. ... P(f_c)</math>, onde <math>f_c</math> é nova. Remova os quantificadores universais. Coloque a fórmula na forma normal conjuntiva. Coloque a sentença resultante na forma de um conjunto de cláusulas, substituindo <math>C_1 \land ... \land C_n</math> por <math>\{C_1, ..., C_n\} </math>. Freqüentemente, é suficiente gerar uma FNC eqüi-satisfatível (não uma equivalente) para uma fórmula. Nesse caso, o pior caso de crescimento exponencial pode ser evitado introduzindo definições e usando-as para renomear partes da fórmula. (pt)
|
![[RDF Data]](http://dbpedia.org/statics/sw-cube.png)
