如何理解约束的偏序答案

【问题标题】：How to understand the partial ordering by constraints如何理解约束的偏序
【发布时间】：2021-06-09 10:19:45
【问题描述】：

约束的偏序规则定义为：
[temp.constr.order#1]

一个约束 P 包含一个约束 Q 当且仅当，对于 P 的析取范式中的每个析取子句 P_i，P_i 包含每个析取子句 Q _j 在 Q 的合取范式中，其中

一个分离子句 P_i 包含一个连接子句 Q_j 当且仅当在 P_ia >i 在 Q_j 中存在原子约束 Q_jb 使得 P_ia 包含 Q_jb，和

一个原子约束 A 包含另一个原子约束 B 当且仅当 A 和 B 使用 [temp.constr.atomic] 中描述的规则相同。

我不知道如何获得给定约束的析取和合取范式。此外，我对第二个项目符号有些困惑。

问题一：

给定一个名为 P 的约束，其形式为 A ∧ B，另一个名为 Q 的约束，形式为 A，其中 A 和 B 都是原子约束。对于约束P 它的析取范式是什么？而Q的合取和析取范式是什么？

问题2：

那P_i和Q_j是取自其析取/合取范式对应位置的从句吗？特别是，当且仅当在 P_i 中存在原子约束 P_ia 且存在原子约束 Q_jb时，如何理解句子> 在 Q_j 中，使得 P_ia 包含 Q_jb？如何解释Qi 具有 Pi 没有的额外原子约束的情况？ P 包含 Q 吗？您能否给出一个阐述过程来解释为什么A ∧ B 包含A？

【问题讨论】：

请添加报价链接。
@largest_prime_is_463035818 已添加。
Somewhat related answer.
@dfrib 是的，我找到了一个很棒的online logic calculator，它可以帮助我将公式转换为它的 CNF 或 DNF，以便分析相关规则。

标签： c++ language-lawyer c++20

【解决方案1】：

A ∧ B 和 A 都已经是析取范式和合取范式。

在这种情况下，P 中有一个分离子句，Q 中有一个连接子句。

然后您检查P0 (A ∧ B) 的任何子句是否包含Q0 (A) 的任何子句，它确实如此（A 包含A）。

【讨论】：

如何获取DNF或CNF？如果P0(A) 而Q0(A V B)，那P0 是否包含Q0？
你必须替换子句，直到你有一个连词的析取（对于 dnf）或一个析取的连词（对于 cnf）。 ((a ^ b) v c) ^ d 是你必须搞砸的一个例子，!(a ^ b)
如果我把你的例子加括号可能会更清楚：P = ((A ∧ B)); P0 = (A ∧ B); P00 = A，P01 = B。 Q = ((A)); Q0 = (A); Q00 = A.
对于第二个子弹，这是否意味着仅存在可以识别为 Qib 的 Pia，然后 Pi 将包含 Qi？比如P0(A)和Q0(A V B)？ P0 会包含 Q0？
是的，因为P00 包含Q00