介词逻辑推理

先决条件：人工智能中的 Wumpus 世界

代理使用逻辑推理来识别哪些方格是安全的，但通过 A ^*搜索制定计划。我们将在这部分向您展示如何使用逻辑推理来构建计划。基本概念很简单：

1. 写一个包含
   • $Init^{0}$ ，一组关于初始状态的声明；
   • $\text { Transition }^{1}, \ldots, \text { Transition }^{t}$ ，所有可能的动作在每个时间的后继状态公理，直到某个最大时间$t$ ;和
   • 目标在某个时间达到的断言$t$ ： $\text { HaveGold }^{t} \wedge \text { Climbed Out }^{t}$
2. 向 SAT 求解器展示整个语句。如果解决方案开发出合适的模型，则可以实现目标；如果该短语不可满足，则计划问题是不可能的。
3. 假设您找到了一个模型，请提取指示操作的变量并将它们设置为 true。它们形成了实现目标的战略。

介词逻辑推理

SATP _LAN是一种命题规划技术。它制定了上述一般概念，但有所不同。该算法尝试每个可能的步数 t，直到某个最大可能的计划长度 Tmax，因为代理不知道达到目标需要多少步。如果以这种方式存在，则可以保证找到最短的计划。由于 SATP _LAN寻找解决方案的方式，该策略不能用于部分可观察的环境； SATP _LAN将简单地将不可观察的变量设置为构建解决方案所需的值。

创建知识库是使用 SATP _LAN的关键步骤。从表面上看，wumpus 世界公理似乎足以满足上述步骤 1(a) 和 1(b) 的要求。蕴涵的要求（由$ASK$ ) 而另一方面，那些可满足性却大不相同。考虑代理的初始位置$[1,1]$ ，并说代理人的适度目标是$[2,1]$在时间 1。 $L_{1,1}^{0}$在初始知识库中，并且$L_{2,1}^{1}$是目标。我们可以建立$L_{2,1}^{1}$使用$ASK$如果 Forward ⁰被肯定，但如果说，Shoot0 被断言，我们不能证明 L12,1。 SATPLAN 现在正在搜索计划 [Forward0]；到目前为止，一切都很好。然而，SATP _LAN也检测到计划 [Shoot ⁰ ]。这怎么可能？为了找出答案，我们检查了 SATPLAN 的模型，其中包括分配$L_{2,1}^{0}$ ，这表明代理可以在时间 1 处于 [2,1] 处，方法是在时间 0 在那里并射击。 “我们不是说特工在吗？ $[1, 1]$在时间 0？有人可能想知道。是的，但是我们没有通知代理不能同时在两个地方！ $L_{2,1}^{0}$蕴涵未知，因此不能用于证明；另一方面， $L_{2,1}^{0}$可满足性未知，因此可以设置为有助于实现目标的任何值。因此，SATPLAN 是一个有用的知识库调试工具，因为它可以识别知识差距。在这种情况下，我们可以通过声明智能体在每个时间步恰好位于一个位置来修复知识库，使用一组类似于用来说明恰好存在一个 wumpus 的短语。对于除$[1, 1]$ , 我们可以声称$\neg L_{x, y}^{0}$ ;位置的后继状态公理负责进一步的时间步长。可以使用相同的调整来确保代理只有一个方向。

另一方面，SATP _LAN有更多惊喜。首先是它寻找执行不可能活动的模型，例如在没有它的情况下射箭。为了理解为什么我们需要仔细研究后继状态公理对具有未满足先决条件的动作的含义。公理在预测如果执行这样的动作不会发生任何事情时是正确的，但在说无法执行该动作时它们是不正确的！为避免产生包含非法行为的计划，我们必须包含前提条件公理，这些公理表明要发生行为，必须满足前提条件。例如，我们需要说$\text { Shoot }^{t} \Rightarrow \text { HaveArrow }^{t}$每次$t$ .

这确保了如果一个计划在任何时间点选择了射击动作，那么代理在那个时候屏幕上必须有一个箭头。多个同时行动的计划制定是 SATP _LAN的第二个惊喜。例如，它可能会生成一个模型，其中 Forward0 和 Shoot0 都为真，这是不允许的。我们引入动作排除公理来解决这个问题：对于每对动作$A_{i}^{t}$和$A_{j}^{t}$ ，我们添加公理$\neg A_{i}^{t} \vee \neg A_{j}^{t}$ .

需要注意的是，同时向前和射击并不困难，但是例如同时射击和抓取是非常不切实际的。我们可以通过仅对真正相互干扰的活动对强加行动排除公理来允许具有许多同时行动的计划——并且由于 SATP _LAN确定了最短的合法计划，我们可以确信它将利用这种能力。

总而言之，SATP _LAN在包含起始状态、目标、后继状态公理、前置条件公理和动作排除公理的句子中查找模型。可以证明，这组公理是足够的，因为不再存在错误的“解决方案”。任何满足命题陈述的模型都是手头问题的可行解决方案。由于现代 SAT 求解技术，该策略相当现实。例如，DPLL 风格的求解器可以轻松地为 wumpus 世界实例提供 11 步求解。

本节讨论的代理构造的声明性方法是代理通过在知识库中断言语句并进行逻辑推理来工作。这种方法的一些缺陷被伪装成“for each time t”和“for each square [x, y]”这些短语必须由自动生成通用句式实例的代码来实现，以便插入到知识库中任何实用的代理。我们可能需要一个$100 X 100$棋盘和 1000 个时间步，用于一个合理大小的 wumpus 世界——类似于一个小型电脑游戏——产生包含数千万或数亿个短语的知识库。这不仅不切实际，而且还突出了一个更大的问题：我们对 wumpus 世界有所了解——即， “物理学”在所有方格和时间步长上都以相同的方式工作——这是我们无法在命题逻辑中明确描述的.我们需要一种更具表现力的语言来应对这一挑战，一种允许以自然方式编写诸如“for each time t”和“for each square [x,y]”之类的词。任何大小和持续时间的 wumpus 世界都可以用大约 10 个句子来描述，而不是一阶逻辑中的一千万或十万亿。