#### 逻辑连接词 #### 模型 #### Model Checking

• 要确定$\mathrm{KB} \vDash \alpha$：
• 列举所有可能的模型。
• 如果在每个模型中$\text{KB}$为真时$α$也为真，则$\text{KB}$蕴含$α$。
• 否则，$\text{KB}$不蕴含$α$。

Model Checking其实就是穷举法，来看一个具体例子： #### 推断法则

$\alpha \rightarrow \beta,\alpha$ $\beta$
$\alpha \wedge \beta$ $\alpha$
$\neg(\neg \alpha)$ $\alpha$
$\alpha \rightarrow \beta$ $\neg \alpha \vee \beta$
$\alpha \leftrightarrow \beta$ $(\alpha \rightarrow \beta) \wedge(\beta \rightarrow \alpha)$
$\neg(\alpha \wedge \beta)$ $\neg \alpha \vee \neg \beta$
$\neg(\alpha \vee \beta)$ $\neg \alpha \wedge \neg \beta$
$(\alpha \wedge(\beta \vee \gamma))$ $(\alpha \wedge \beta) \vee(\alpha \wedge \gamma)$
$(\alpha \vee(\beta \wedge \gamma))$ $(\alpha \vee \beta) \wedge(\alpha \vee \gamma)$

• 初始状态：起始知识库
• 动作：推理规则
• 转移模型：推断后的新知识库
• 目标测试：坚持我们试图证明的命题
• 路径成本函数：证明中的步骤数

#### Resolution

$P \vee Q_{I} \vee Q_{2} \vee \ldots \vee Q_{n},\neg P$ $Q_{I} \vee Q_{2} \vee \ldots \vee Q_{n}$
$\alpha \wedge \beta$ $\alpha$
$P \vee Q ,\neg P \vee R$ $Q \vee R$
$\alpha \rightarrow \beta$ $\neg \alpha \vee \beta$
$P \vee Q_{I} \vee Q_{2} \vee \ldots \vee Q_{n},\neg P \vee R_{I} \vee R_{2} \vee \ldots \vee R_{m}$ $Q_{I} \vee Q_{2} \vee \ldots \vee Q_{n} \vee R_{I} \vee R_{2} \vee \ldots \vee R_{m}$

#### Inference by Resolution

• 要确定$\mathrm{KB} \vDash \alpha$：
• 将$(\mathrm{KB} \wedge \neg \alpha)$转换为合取范式。
• 检查是否可以使用Resolution来产生一个新的句子。
• 如果我们产生空子句（等价于False），我们产生矛盾，即$\mathrm{KB} \vDash \alpha$。
• 否则，如果我们无法添加新子句，则没有蕴含关系。

### Project

#### Knights

AKnight = Symbol("A is a Knight")
AKnave = Symbol("A is a Knave")

BKnight = Symbol("B is a Knight")
BKnave = Symbol("B is a Knave")

CKnight = Symbol("C is a Knight")
CKnave = Symbol("C is a Knave")

# Puzzle 0
# A says "I am both a knight and a knave."
knowledge0 = And(
Or(And(AKnight, And(AKnight, AKnave)), And(AKnave, Not(And(AKnight, AKnave)))),
#有且只有一个为真
Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
)

# Puzzle 1
# A says "We are both knaves."
# B says nothing.
knowledge1 = And(
Or(And(AKnight, And(AKnave, BKnave)), And(AKnave, Not(And(AKnave, BKnave)))),
#有且只有一个为真
Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
)

# Puzzle 2
# A says "We are the same kind."
# B says "We are of different kinds."
knowledge2 = And(
Or(And(AKnight, BKnight), And(AKnave, BKnight)),
Or(And(BKnight, AKnave), And(BKnave, AKnave)),
#有且只有一个为真
Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
)

# Puzzle 3
# A says either "I am a knight." or "I am a knave.", but you don't know which.
# B says "A said 'I am a knave'."
# B says "C is a knave."
# C says "A is a knight."
#Or(And(AKnight, AKnave), And(AKnave, AKnight))
knowledge3 = And(
Or(And(AKnight, Or(AKnight, AKnave)), And(AKnave, Not(Or(AKnight, AKnave)))),
Or(And(BKnight, Or(And(AKnight, AKnave), And(AKnave, AKnight))), And(BKnave, Not(Or(And(AKnight, AKnave), And(AKnave, AKnight))))),
Or(And(BKnight, CKnave), And(BKnave, CKnight)),
Or(And(CKnight, AKnight), And(CKnave, AKnave)),
#有且只有一个为真
Or(And(AKnight, Not(AKnave)), And(AKnave, Not(AKnight))),
Or(And(BKnight, Not(BKnave)), And(BKnave, Not(BKnight))),
Or(And(CKnight, Not(CKnave)), And(CKnave, Not(CKnight)))
)

#### Minesweeper

Sentence

class Sentence():
"""
Logical statement about a Minesweeper game
A sentence consists of a set of board cells,
and a count of the number of those cells which are mines.
"""

def __init__(self, cells, count):
self.cells = set(cells)
self.count = count

def __eq__(self, other):
return self.cells == other.cells and self.count == other.count

def __str__(self):
return f"{self.cells} = {self.count}"

def known_mines(self):
"""
Returns the set of all cells in self.cells known to be mines.
"""
#raise NotImplementedError
if len(self.cells) == self.count:
if len(self.cells) != 0:
return self.cells

return None

def known_safes(self):
"""
Returns the set of all cells in self.cells known to be safe.
"""
#raise NotImplementedError
if self.count == 0:
if len(self.cells) != 0:
return self.cells

return None

def mark_mine(self, cell):
"""
Updates internal knowledge representation given the fact that
a cell is known to be a mine.
"""
#raise NotImplementedError
if cell in self.cells:
self.cells.remove(cell)
self.count -= 1

def mark_safe(self, cell):
"""
Updates internal knowledge representation given the fact that
a cell is known to be safe.
"""
#raise NotImplementedError
if cell in self.cells:
self.cells.remove(cell)

MinesweeperAI

class MinesweeperAI():
"""
Minesweeper game player
"""

def __init__(self, height=8, width=8):

# Set initial height and width
self.height = height
self.width = width

# Keep track of which cells have been clicked on

# Keep track of cells known to be safe or mines
self.mines = set()
self.safes = set()

# List of sentences about the game known to be true
self.knowledge = []

def mark_mine(self, cell):
"""
Marks a cell as a mine, and updates all knowledge
to mark that cell as a mine as well.
"""
for sentence in self.knowledge:
sentence.mark_mine(cell)

def mark_safe(self, cell):
"""
Marks a cell as safe, and updates all knowledge
to mark that cell as safe as well.
"""
for sentence in self.knowledge:
sentence.mark_safe(cell)

"""
Called when the Minesweeper board tells us, for a given
safe cell, how many neighboring cells have mines in them.

This function should:
1) mark the cell as a move that has been made
2) mark the cell as safe
3) add a new sentence to the AI's knowledge base
based on the value of cell and count
4) mark any additional cells as safe or as mines
if it can be concluded based on the AI's knowledge base
5) add any new sentences to the AI's knowledge base
if they can be inferred from existing knowledge
"""
#raise NotImplementedError
#1
#2
self.mark_safe(cell)
#3
cells = []
for i in range(cell - 1, cell + 2):
for j in range(cell - 1, cell + 2):

# Ignore the cell itself
if (i, j) == cell:
continue

# Update count if cell in bounds and is mine
if 0 <= i < self.height and 0 <= j < self.width:
#已统计的无需考虑
if (i, j) in self.mines:
count -= 1
elif (i, j) not in self.safes:
cells.append((i, j))
self.knowledge.append(Sentence(cells, count))
#4
for sentence in self.knowledge:
safe = sentence.known_safes()
mine = sentence.known_mines()
if safe != None:
self.safes = self.safes.union(safe)
if mine != None:
self.mines = self.mines.union(mine)
#5
n = len(self.knowledge)
for i in range(n):
for j in range(i + 1, n):
s1 = self.knowledge[i]
s2 = self.knowledge[j]
if s1.cells.issubset(s2.cells):
cells = s2.cells - s1.cells
s = Sentence(s2.cells - s1.cells, s2.count - s1.count)
#判断是否重复
if s not in self.knowledge:
self.knowledge.append(s)
elif s2.cells.issubset(s1.cells):
cells = s1.cells - s2.cells
s = Sentence(s1.cells - s2.cells, s1.count - s2.count)
#判断是否重复
if s not in self.knowledge:
self.knowledge.append(s)

def make_safe_move(self):
"""
Returns a safe cell to choose on the Minesweeper board.
The move must be known to be safe, and not already a move

This function may use the knowledge in self.mines, self.safes
and self.moves_made, but should not modify any of those values.
"""
#raise NotImplementedError
for cell in self.safes:
return cell

return None

def make_random_move(self):
"""
Returns a move to make on the Minesweeper board.
Should choose randomly among cells that:
1) have not already been chosen, and
2) are not known to be mines
"""
#raise NotImplementedError
for i in range(self.height):
for j in range(self.width):
if (i, j) not in self.moves_made and (i, j) not in self.mines:
return (i, j)

return None