知识

Conjunctive Normal Form

Definitions：

literal

alt

conjunctive normal form (CNF)

alt

Note:

alt

Examples of CNFs:

alt

Not in CNF:

alt

Validity of a Disjunction of Literals

Lemma:

alt Proof: alt

Satisfiability

Definition:

公式ψ是可满足的，如果存在对其命题原子的真值赋值，使得Φ为真。

Proposition:

这是一个简单但非常有用的结果。 alt Proof: alt

Useful Identities (Boolean Algebra)

alt

A Procedure to Compute CNFs

alt alt alt alt

我们提出了一种算法来计算与给定任意公式Φ等价的CNF公式。该算法是确定性的，并为任何公式计算唯一的CNF。

该算法描述为：

CNF(NNF(IMPL FREE(Φ)))

对于给定的公式Φ。稍后将讨论CNF、NNF和IMPL_FREE函数。

我们将公式转换为CNF，以便于检查其有效性。

为了检查CNF是否有效，我们只需检查每个共轭中是否有p而不是p。

IMPL_FREE

alt

IMPL_FREE Example

alt

NNF

alt

NNF Example

alt

DISTR

alt

CNF

alt

CNF Example

alt

Horn Clauses

Horn Clauses具有有效的可满足性决定方法，是逻辑编程的基础。

Definitions:

Horn Clause

alt

Horn formula

alt

HORN

Theorem

定理：HORN算法是正确的：当给定的HORN公式是可满足的时，它总是终止，并且它的答案是“可满足的”。 alt alt

Horn Clauses Examples

Examples (yes)

alt

Examples (no)

alt

作业

2.1 通过证明以下情况，补充命题逻辑的可靠性和完整性证明：

对于可靠性证明，请完成以下证明规则案例的证明：

alt

对于完整性证明，请完成以下情况的证明：

alt alt

2.2 将以下公式转换为CNF

alt

Φ

¬(p⟶(¬(q⋀(¬p⟶(q⋀r)))))

IMPL_FREE
IMPL_FREE(Φ)=IMPL_FREE(¬(p⟶(¬(q⋀(¬p⟶(q⋀r)))))))
=¬(IMPL_FREE(p⟶(¬(q⋀(¬p⟶(q⋀r))))))[case ¬Φ]
=¬(¬IMPL_FREE(p)⋁IMPL_FREE(¬(q⋀(¬p⟶(q⋀r)))))[case Φ1⟶Φ2]
=¬(¬p⋁¬(IMPL_FREE(q⋀(¬p⟶(q⋀r)))))[case ¬Φ]
=¬(¬p⋁¬(IMPL_FREE(q)⋀IMPL_FREE(¬p⟶(q⋀r)))))[case Φ1⋀Φ2]
=¬(¬p⋁¬(q⋀¬IMPL_FREE(¬p)⋁IMPL_FREE(q⋀r)))[case Φ1⟶Φ2]
=¬(¬p⋁¬(q⋀¬¬IMPL_FREE(p)⋁IMPL_FREE(q)⋀IMPL_FREE(r)))[case ¬Φ][case Φ1⋀Φ2]
=¬(¬p⋁¬(q⋀p⋁q⋀r))
NNF
NNF(IMPL_FREE(Φ))=NNF(¬(¬p⋁¬(q⋀p⋁q⋀r)))
=NNF(¬(¬p)⋀¬(¬(q⋀p⋁q⋀r)))[case Φ1⋁Φ2]
=NNF(p⋀(q⋀p⋁q⋀r))
=NNF(p)⋀NNF(q⋀p⋁q⋀r)[case Φ1⋀Φ2]
=p⋀q⋀p⋁q⋀r

用Horn算法确定下列公式的)=可满足性 alt