In logic, the clause form or normal clause form describes a formula in conjunctive normal form (CNF) in which the conjunctions are each summarized in set notation.
A formula in clause form (seldom also clause form) is a logical combination of literals , notated as disjunctive normal form or conjunctive normal form , whereby it is specified that the empty generalized disjunction interprets the truth value false and the empty generalized conjunction interprets the truth value true.
Normal forms of clauses can be created using a transformation and are used for machine evidence using logical formulas.
example 1
(
(
a
∨
b
)
∧
(
b
∨
c
)
∧
(
a
∨
¬
d
∨
¬
e
)
∧
d
)
{\ displaystyle ((a \ vee b) \ wedge (b \ vee c) \ wedge (a \ vee \ neg d \ vee \ neg e) \ wedge d)}
is a formula in CNF, which is simply represented in clause form as follows:
{
{
a
,
b
}
,
{
b
,
c
}
,
{
a
,
¬
d
,
¬
e
}
,
{
d
}
}
{\ displaystyle \ {\ {a, b \}, \ {b, c \}, \ {a, \ neg d, \ neg e \}, \ {d \} \}}
Example 2 The propositional formula should be transformed into the conjunctive clause form (generalized conjunction):
¬
(
P
∨
(
¬
(
P
∧
Q
)
∧
¬
R.
)
)
{\ displaystyle \ neg (P \ lor (\ neg (P \ land Q) \ land \ neg R))}
{
¬
(
P
∨
(
¬
(
P
∧
Q
)
∧
¬
R.
)
)
}
{\ displaystyle \ {\ neg (P \ lor (\ neg (P \ land Q) \ land \ neg R)) \}}
{
{
¬
P
}
,
{
¬
(
¬
(
P
∧
Q
)
∧
¬
R.
)
}
}
{\ displaystyle \ {\ {\ neg P \}, \ {\ neg (\ neg (P \ land Q) \ land \ neg R) \} \}}
{
{
¬
P
}
,
{
¬
¬
(
P
∧
Q
)
,
¬
¬
R.
}
}
{\ displaystyle \ {\ {\ neg P \}, \ {\ neg \ neg (P \ land Q), \ neg \ neg R \} \}}
{
{
¬
P
}
,
{
(
P
∧
Q
)
,
R.
}
}
{\ displaystyle \ {\ {\ neg P \}, \ {(P \ land Q), R \} \}}
{
{
¬
P
}
,
{
P
,
R.
}
,
{
Q
,
R.
}
}
{\ displaystyle \ {\ {\ neg P \}, \ {P, R \}, \ {Q, R \} \}}
Horn clauses Horn clauses represent a special normal form of clauses in which each clause contains a maximum of one positive literal .
negative Horn clause: clause does not contain a positive literal
positive Horn clause: clause contains a positive literal
This notation is popular because Horn clauses can be quickly transformed into a number of implications.
example
Horn clause:
{
{
a
,
¬
b
}
,
{
¬
c
,
¬
d
}
,
{
b
}
}
{\ displaystyle \ {\ {a, \ neg b \}, \ {\ neg c, \ neg d \}, \ {b \} \}}
Equivalent expression:
(
¬
a
⇒
¬
b
)
∧
(
c
⇒
¬
d
)
∧
(
t
r
u
e
⇒
b
)
{\ displaystyle (\ neg a \ Rightarrow \ neg b) \ wedge (c \ Rightarrow \ neg d) \ wedge (true \ Rightarrow b)}
Further possible notation:
(
b
⇒
a
)
∧
(
c
∧
d
⇒
f
a
l
s
e
)
∧
(
t
r
u
e
⇒
b
)
{\ displaystyle (b \ Rightarrow a) \ wedge (c \ wedge d \ Rightarrow false) \ wedge (true \ Rightarrow b)}
<img src="https://de.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">
