# 程序示例——命题逻辑与模型检测
::: warning 😋
阅读程序中涉及命题逻辑的部分，然后“玩一玩”程序！

完成习题
:::

::: tip 📥
本节附件下载 <Download url="https://pic-hdu-cs-wiki-1307923872.cos.ap-shanghai.myqcloud.com/code/2-Lecture.zip"/>
:::
# Sentence——父类

```python
class Sentence(): # 父类
    def evaluate(self, model):
        """计算逻辑表达式的值"""
        raise Exception("nothing to evaluate")
    def formula(self):
        """返回表示逻辑表达式的字符串形式。"""
        return ""
    def symbols(self):
        """返回逻辑表达式中所有命题符号的集合。"""
        return set()
    @classmethod # @classmethod装饰器 使得类方法可以在类上被调用 Sentence.validate(...)
    def validate(cls, sentence):
        """验证操作数是否是Sentence或其子类"""
        if not isinstance(sentence, Sentence):
            raise TypeError("must be a logical sentence")
    @classmethod # @classmethod装饰器 使得类方法可以在类上被调用 Sentence.parenthesize(...)
    def parenthesize(cls, s):
        """如果表达式尚未加圆括号，则加圆括号。"""
        def balanced(s):
            """检查字符串是否有配对的括号。"""
            count = 0
            for c in s:
                if c == "(":
                    count += 1
                elif c == ")":
                    if count <= 0:
                        return False
                    count -= 1
            return count == 0
        if not len(s) or s.isalpha() or (s[0] == "(" and s[-1] == ")" and balanced(s[1:-1])):
            return s
        else:
            return f"({s})"
```

# Symbol——命题符号类

```python
class Symbol(Sentence):
    def __init__(self, name):
        """初始化命题符号"""
        self.name = name
    def __eq__(self, other):
        """定义命题符号的相等"""    
        return isinstance(other, Symbol) and self.name == other.name
    ...
    def evaluate(self, model):
        """命题符号在模型中赋值"""
        try:
            return bool(model[self.name])
        except KeyError:
            raise EvaluationException(f"variable {self.name} not in model")
    def formula(self):
        """返回表示命题符号的字符串形式。"""
        return self.name
    def symbols(self):
        """返回命题符号的集合。"""
        return {self.name}
```

# Not——逻辑非类

```python
class Not(Sentence):
    def __init__(self, operand):
        """验证操作数是否是Sentence或其子类"""
        Sentence.validate(operand)
        self.operand = operand
    def __eq__(self, other):
        """定义相等"""
        return isinstance(other, Not) and self.operand == other.operand
    ...
    def evaluate(self, model):
        """逻辑非在模型中的赋值"""
        return not self.operand.evaluate(model)
    def formula(self):
        """返回表示逻辑非的字符串形式"""
        return "¬" + Sentence.parenthesize(self.operand.formula())
    def symbols(self):
        """返回逻辑非中的命题符号的集合"""
        return self.operand.symbols()
```

# And——逻辑乘类

```python
class And(Sentence):
    def __init__(self, *conjuncts):
        for conjunct in conjuncts:
        """验证操作数是否是Sentence或其子类"""
            Sentence.validate(conjunct)
        self.conjuncts = list(conjuncts)
    def __eq__(self, other):
        """定义相等"""    
        return isinstance(other, And) and self.conjuncts == other.conjuncts
    def add(self, conjunct):
        """添加命题"""
        Sentence.validate(conjunct)
        self.conjuncts.append(conjunct)
    def evaluate(self, model):
        """逻辑乘在模型中的赋值"""
        return all(conjunct.evaluate(model) for conjunct in self.conjuncts)
    def formula(self):
        """返回表示逻辑乘的字符串形式"""
        if len(self.conjuncts) == 1:
            return self.conjuncts[0].formula()
        return " ∧ ".join([Sentence.parenthesize(conjunct.formula())
                           for conjunct in self.conjuncts])
    def symbols(self):
        """"返回逻辑乘中的所有命题符号的集合"""
        return set.union(*[conjunct.symbols() for conjunct in self.conjuncts])
```

# Or——逻辑和类

```python
class Or(Sentence):
    def __init__(self, *disjuncts):
        for disjunct in disjuncts:
        """验证操作数是否是Sentence或其子类"""
            Sentence.validate(disjunct)
        self.disjuncts = list(disjuncts)
    def __eq__(self, other):
        """定义相等"""    
        return isinstance(other, Or) and self.disjuncts == other.disjuncts
    ...
    def evaluate(self, model):
         """逻辑和在模型中的赋值"""
        return any(disjunct.evaluate(model) for disjunct in self.disjuncts)
    def formula(self):
        """返回表示逻辑和的字符串形式"""
        if len(self.disjuncts) == 1:
            return self.disjuncts[0].formula()
        return " ∨  ".join([Sentence.parenthesize(disjunct.formula())
                            for disjunct in self.disjuncts])
    def symbols(self):
        """"返回逻辑乘中的所有命题符号的集合"""
        return set.union(*[disjunct.symbols() for disjunct in self.disjuncts])
```

# Implication——逻辑蕴含类

```python
class Implication(Sentence):
    def __init__(self, antecedent, consequent):
        """验证操作数是否是Sentence或其子类"""
        Sentence.validate(antecedent)
        Sentence.validate(consequent)
        """前件"""
        self.antecedent = antecedent
        """后件"""
        self.consequent = consequent
    def __eq__(self, other):
        """定义相等"""
        return (isinstance(other, Implication)
                and self.antecedent == other.antecedent
                and self.consequent == other.consequent)
    ...
    def evaluate(self, model):
        """逻辑蕴含在模型中的赋值"""
        return ((not self.antecedent.evaluate(model))
                or self.consequent.evaluate(model))
    def formula(self):
        """返回表示逻辑蕴含的字符串形式"""
        antecedent = Sentence.parenthesize(self.antecedent.formula())
        consequent = Sentence.parenthesize(self.consequent.formula())
        return f"{antecedent} => {consequent}"
    def symbols(self):
        """"返回逻辑蕴含中的所有命题符号的集合"""
        return set.union(self.antecedent.symbols(), self.consequent.symbols())
```

# Biconditional——逻辑等值类

```python
class Biconditional(Sentence):
    def __init__(self, left, right):
        """验证操作数是否是Sentence或其子类"""
        Sentence.validate(left)
        Sentence.validate(right)
        self.left = left
        self.right = right
    def __eq__(self, other):
        """定义相等"""
        return (isinstance(other, Biconditional)
                and self.left == other.left
                and self.right == other.right)
    ...
    def evaluate(self, model):
        """逻辑等值在模型中的赋值"""
        return ((self.left.evaluate(model)
                 and self.right.evaluate(model))
                or (not self.left.evaluate(model)
                    and not self.right.evaluate(model)))
    def formula(self):
        """返回表示逻辑等值的字符串形式"""
        left = Sentence.parenthesize(str(self.left))
        right = Sentence.parenthesize(str(self.right))
        return f"{left} <=> {right}"
    def symbols(self):
        """"返回逻辑等值中的所有命题符号的集合"""
        return set.union(self.left.symbols(), self.right.symbols())
```

# Model_check()——模型检测算法

```python
def model_check(knowledge, query):
    """
    检查知识库是否推理蕴含查询结论。
    >>> p = Symbol("p")
    >>> q = Symbol("q")
    >>> r = Symbol("r")
    >>> knowledge = And(p, q, Implication(And(p, q), r))
    >>> knowledge.formula()
    'p ∧ q ∧ ((p ∧ q) => r)'
    >>> query = r
    >>> model_check(knowledge,query)
    True
    """
    def check_all(knowledge, query, symbols, model):
        """检查给定特定模型的知识库是否推理蕴含查询结论。"""
        # 如果模型已经为所有的命题符号赋值
        if not symbols:  # symbols为空即所有 symbols都在模型中被赋值
            # 若模型中的知识库为真，则查询结论也必须为真
            if knowledge.evaluate(model):
                return query.evaluate(model)
            return True
        else:
            # 递归生成并检测所有模型
            # 选择其余未使用的命题符号之一
            remaining = symbols.copy()
            p = remaining.pop()
            # 创建一个命题符号为true的模型
            model_true = model.copy()
            model_true[p] = True
            # 创建一个命题符号为false的模型
            model_false = model.copy()
            model_false[p] = False
            # 确保在两种模型中都进行蕴含推理
            return (check_all(knowledge, query, remaining, model_true) and
                    check_all(knowledge, query, remaining, model_false))
    # 获取知识库和查询结论中的所有命题符号
    symbols = set.union(knowledge.symbols(), query.symbols())
    # 进行模型检测
    return check_all(knowledge, query, symbols, dict())
```

# 线索游戏

在游戏中，一个人在某个地点使用工具实施了谋杀。人、工具和地点用卡片表示。每个类别的一张卡片被随机挑选出来，放在一个信封里，由参与者来揭开真相。参与者通过揭开卡片并从这些线索中推断出信封里必须有什么来做到这一点。我们将使用之前的模型检查算法来揭开这个谜团。在我们的模型中，我们将已知与谋杀有关的项目标记为 True，否则标记为 False。

```python
import termcolor
from logic import *
mustard = Symbol("ColMustard")
plum = Symbol("ProfPlum")
scarlet = Symbol("MsScarlet")
characters = [mustard, plum, scarlet]

ballroom = Symbol("ballroom")
kitchen = Symbol("kitchen")
library = Symbol("library")
rooms = [ballroom, kitchen, library]

knife = Symbol("knife")
revolver = Symbol("revolver")
wrench = Symbol("wrench")
weapons = [knife, revolver, wrench]

symbols = characters + rooms + weapons
def check_knowledge(knowledge):
    for symbol in symbols:
        if model_check(knowledge, symbol):
            termcolor.cprint(f"{symbol}: YES", "green")
        elif not model_check(knowledge, Not(symbol)):
            # 模型检测无法确定知识库可以得出 Not(symbol) 即 symbol是可能的
            print(f"{symbol}: MAYBE")
        else:
            termcolor.cprint(f"{symbol}: No", "red")
# 必须有人、房间和武器。
knowledge = And(
    Or(mustard, plum, scarlet),
    Or(ballroom, kitchen, library),
    Or(knife, revolver, wrench)
)
# 初始卡牌
knowledge.add(And(
    Not(mustard), Not(kitchen), Not(revolver)
))
# 未知卡牌
knowledge.add(Or(
    Not(scarlet), Not(library), Not(wrench)
))
# 已知卡牌
knowledge.add(Not(plum))
knowledge.add(Not(ballroom))
check_knowledge(knowledge)
```

# Mastermind 游戏

在这个游戏中，玩家一按照一定的顺序排列颜色，然后玩家二必须猜测这个顺序。每一轮，玩家二进行猜测，玩家一返回一个数字，指示玩家二正确选择了多少颜色。让我们用四种颜色模拟一个游戏。假设玩家二猜测以下顺序：

![](https://pic-hdu-cs-wiki-1307923872.cos.ap-shanghai.myqcloud.com/FZCJbOzr9o4oQPx7SNGcFxTSnRd.png)

玩家一回答“二”。因此，我们知道其中一些两种颜色位于正确的位置，而另两种颜色则位于错误的位置。根据这些信息，玩家二试图切换两种颜色的位置。

![](https://pic-hdu-cs-wiki-1307923872.cos.ap-shanghai.myqcloud.com/Y80wbn96sol7PUxO5fKcOA9Hnbg.png)

现在玩家一回答“零”。因此，玩家二知道切换后的颜色最初位于正确的位置，这意味着未被切换的两种颜色位于错误的位置。玩家二切换它们。

![](https://pic-hdu-cs-wiki-1307923872.cos.ap-shanghai.myqcloud.com/EuXObldHcoaO74xIzZocQQKTn4k.png)

在命题逻辑中表示这一点需要我们有(颜色的数量)$^2$个原子命题。所以，在四种颜色的情况下，我们会有命题 red0，red1，red2，red3，blue0…代表颜色和位置。下一步是用命题逻辑表示游戏规则（每个位置只有一种颜色，没有颜色重复），并将它们添加到知识库中。最后一步是将我们所拥有的所有线索添加到知识库中。在我们的案例中，我们会补充说，在第一次猜测中，两个位置是错误的，两个是正确的，而在第二次猜测中没有一个是对的。利用这些知识，模型检查算法可以为我们提供难题的解决方案。

```python
from logic import *
colors = ["red", "blue", "green", "yellow"]
symbols = []
for i in range(4):
    for color in colors:
        symbols.append(Symbol(f"{color}{i}"))
knowledge = And()
# 每种颜色都有一个位置。
for color in colors:
    knowledge.add(Or(
        Symbol(f"{color}0"),
        Symbol(f"{color}1"),
        Symbol(f"{color}2"),
        Symbol(f"{color}3")
    ))
# 每种颜色只有一个位置。
for color in colors:
    for i in range(4):
        for j in range(4):
            if i != j:
                knowledge.add(Implication(
                    Symbol(f"{color}{i}"), Not(Symbol(f"{color}{j}"))
                ))
# 每个位置只有一种颜色。
for i in range(4):
    for c1 in colors:
        for c2 in colors:
            if c1 != c2:
                knowledge.add(Implication(
                    Symbol(f"{c1}{i}"), Not(Symbol(f"{c2}{i}"))
                ))
knowledge.add(Or(
    And(Symbol("red0"), Symbol("blue1"), Not(Symbol("green2")), Not(Symbol("yellow3"))),
    And(Symbol("red0"), Symbol("green2"), Not(Symbol("blue1")), Not(Symbol("yellow3"))),
    And(Symbol("red0"), Symbol("yellow3"), Not(Symbol("blue1")), Not(Symbol("green2"))),
    And(Symbol("blue1"), Symbol("green2"), Not(Symbol("red0")), Not(Symbol("yellow3"))),
    And(Symbol("blue1"), Symbol("yellow3"), Not(Symbol("red0")), Not(Symbol("green2"))),
    And(Symbol("green2"), Symbol("yellow3"), Not(Symbol("red0")), Not(Symbol("blue1")))
))
knowledge.add(And(
    Not(Symbol("blue0")),
    Not(Symbol("red1")),
    Not(Symbol("green2")),
    Not(Symbol("yellow3"))
))
print(knowledge.formula())
for symbol in symbols:
    if model_check(knowledge, symbol):
        print(symbol)
```

# Quiz

1. 下面的问题将问你关于以下逻辑句子的问题。 1.如果 Hermione 在图书馆，那么 Harry 在图书馆。 2.Hermione 在图书馆里。 3.Ron 在图书馆，Ron 不在图书馆。 4.Harry 在图书馆。 5.Harry 不在图书馆，或者 Hermione 在图书馆。 6.Rom 在图书馆，或者 Hermione 在图书馆。

    以下哪一个逻辑蕴含推理是正确的？

   1. $1\vDash 4$
   2. $5\vDash 6$
   3. $1\vDash 2$
   4. $6\vDash 2$
   5. $2\vDash 5$
   6. $6\vDash 3$

2. 除了讲义上讨论的连接词之外，还有其他的逻辑连接词。其中最常见的是“异或”（用符号$\oplus$表示）。表达式$A\oplus B$表示句子“A 或 B，但不是两者都有。”以下哪一个在逻辑上等同于$A\oplus B$？
   1. $(A ∨ B) ∧ ¬ (A ∨ B)$
   2. $(A ∨ B) ∧ (A ∧ B)$
   3.  $(A ∨ B) ∧ ¬ (A ∧ B)$
   4.  $(A ∧ B) ∨ ¬ (A ∨ B)$

3.  设命题变量$R$为“今天下雨”，变量$C$为“今天多云”，变量$S$ 为“今天晴”。下面哪一个是“如果今天下雨，那么今天多云但不是晴天”这句话的命题逻辑表示？

    1.  $(R → C) ∧ ¬S$
    2.  $R → C → ¬S$
    3.  $R ∧ C ∧ ¬S$
    4.  $R → (C ∧ ¬S)$
    5.  $(C ∨ ¬S) → R$

4.  在一阶逻辑中，考虑以下谓词符号。$Student(x)$表示“x 是学生”的谓词。$Course(x)$代表“x 是课程”的谓词，$Enrolled(x,y)$表示“x 注册了 y”的谓词以下哪一项是“有一门课程是 Harry 和 Hermione 都注册的”这句话的一阶逻辑翻译？
    1.  $∀x(Course(x)∧Enrolled(Harry, x) ∧ Enrolled(Hermione, x))$
    2.  $∀x(Enrolled(Harry, x) ∨ Enrolled(Hermione, x))$
    3.  $∀x(Enrolled(Harry, x) ∧ ∀y Enrolled(Hermione, y))$
    4.  $∃xEnrolled(Harry, x) ∧ ∃y Enrolled(Hermione, y)$
    5.  $∃x(Course(x) ∧ Enrolled(Harry, x) ∧ Enrolled(Hermione, x))$
    6.  $∃x(Enrolled(Harry, x) ∨ Enrolled(Hermione, x))$