Assignment

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

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

∧e1

Solution

alt，其中alt出现在l<k行。公式alt具有较短的证明，因此使用归纳假设，它具有真值T。根据∧的真值表，我们可以得出结论，alt具有真值T。

∧e2

Solution

同上。

⊥e

Solution

⊥ 出现在第l<k行。这意味着我们在alt行出现alt。利用归纳假设，alt同时具有真值T。在这样的真值表中，任何公式都可以有真值T。

¬i

Solution

alt，以φ作为第l<k行的假设，以及⊥ 出现在第m<k行，alt。如果φ是T，那么归纳假设告诉我们⊥ 是T，因为它有较短的证明，并且alt中的所有假设都是T。因此，在这样的真值表中，任何公式都可以是T，包括alt。如果φ是F，那么根据真值表，φ是T，这意味着alt是T。

¬¬e 

Solution

∨i1

Solution

∨i2

Solution

→ i

Solution

¬e

Solution

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

将以下公式转换为CNF

¬(p → (¬(q∧(¬p → (q∧r)))))

Solution

IMPL_FREE

IMPL_FREE(¬(p → (¬(q∧(¬p → (q∧r))))))

=¬(¬p∨(¬(q∧IMPL_FREE(¬p → (q∧r)))))

=¬(¬p∨(¬(q∧(¬¬p∨(q∧r)))))

NNF

NNF(¬(¬p∨(¬(q∧(¬¬p∨(q∧r))))))

=NNF(¬¬p)∧NNF(¬¬(q∧(¬¬p∨(q∧r))))

=p∧(q∧NNF(¬¬p∨(q∧r)))

=p∧(q∧(p∨(q∧r)))

CNF

CNF(p∧(q∧(p∨(q∧r)))

=p∧q∧CNF(p∨(q∧r))

=p∧q∧DISTR(p,CNF(q∧r))

=p∧q∧DISTR(p,q)∧DISTR(p,r)

=p∧q∧(p∨q)∧(p∨r)

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

(p∧q∧s → ⊥) ∧ (q∧s → p) ∧ (⊤ → s) ∧ (s → q)

Solution

步骤 标记 条件
1 {s} ⊤ → s
2 {s,q} s → q
3 {s,q,p} q∧s → p
4 {s,q,p,⊥} p∧q∧s → ⊥

结论：不满意