微信搜索“高速商务通”，马上办理ETC
在数学中，自动定理证明用于某些特定任务。例如，图论的重要四色定理首先在一个特殊的证明者的帮助下于1976年证明。然而，自动化的证明者仍然在数学中扮演次要角色。
另一方面，在AI开始时，谓词逻辑对于实际应用中专家系统的开发非常重要。由于建模不确定性存在问题（见第4.4节），如今的专家系统通常使用其他形式来开发。
今天，逻辑在验证任务中扮演着越来越重要的角色。自动程序验证是目前人工智能与软件工程之间的重要研究领域。越来越复杂的软件系统正在接管任务
越来越多的责任和安全相关性。这里需要证明程序的某些安全特性。这样的证明不能通过测试完成的程序来实现，因为通常不可能将程序应用于所有可能的输入。因此，这是一般甚至专用推理系统的理想领域。除此之外，目前正在使用加密协议，其安全特性已经自动验证[FS97，Sch01]。使用自动化证明器的另一个挑战是软件和硬件的合成。例如，为此，证明者应该支持软件工程师从规范生成程序。
对于当今的许多程序员来说，软件重用也非常重要。程序员查找一个程序，该程序获取具有某些属性的输入数据，并计算具有所需属性的结果。排序算法接受具有特定数据类型的条目的输入数据，并且从这些条目创建这些条目的排列，其具有每个元素小于或等于下一个元素的属性。程序员首先在PL1中制定查询规范，由两部分组成。第一部分PREQ包括在应用所需程序之前必须保持的前提条件。第二部分POSTQ包含后置条件，在应用所需程序后必须保留。
在下一步中，必须搜索软件数据库以查找满足这些要求的模块。要正式检查，数据库必须为每个模块M存储前置条件PREM和后置条件POSTM的正式描述。关于模块能力的假设是模块的前提条件遵循查询的前提条件。它必须坚持这一点
PREQ ⇒ PREM。
作为应用模块M的先决条件所需的所有条件必须在查询中显示为前提条件。例如，如果数据库中的模块只接受整数列表，那么作为输入的整数列表也必须在查询中显示为前提条件。查询中的另一个要求，例如，只显示偶数，不会导致问题。
此外，它必须适用于后置条件
POSTM ⇒ POSTQ。
也就是说，在应用模块之后，必须满足查询所需的所有属性。我们现在在[Sch01]的一个例子中展示了一个定理证明器在这个任务中的应用。
例3.8维也纳发展方法规范语言VDM-SL经常被用作规则前后条件的语言。假设在软件数据库中，模块R OTATE的描述是可用的，其将第一列表元素移动到列表的末尾。我们正在寻找一个模块S HUFFLE，它可以创建列表的任意排列。这两个规格读了
|
R OTATE（l ： List）l ：列表 预真 岗位 （L = []⇒升= []）∧ （L = []⇒升=（尾升）[ 头升]） |
S HUFFLE（x ： List）x ：列表 预真 后 ∀ 我：项目 ・ （∃ X 1，X 2 ：列表・ X = X 1 [我] X 2 ⇔ ∃ ÿ 1，Y 2 ：列表・ X = ÿ 1 [我] ÿ 2） |
・
⇒∧⇒
这里“”代表列表的串联，“”将量词与其变量与公式的其余部分分开。函数“head l ”和“tail l ”分别从列表中选择第一个元素和其余元素。SHUFFLE的规范表明在应用SHUFFLE之前列表（x）中的每个列表元素i必须在应用之后的结果（x）中，反之亦然。现在必须显示公式（PREQ PREM）（POSTM POSTQ）是包含数据类型列表描述的知识库的结果。两个VDM-SL规范产生了验证任务
∀ L，L，X，X：列表 ・ （L = X ∧ 升 = X ∧ （瓦特 ⇒ 瓦特）） ∧
（L = X ∧升= X ∧（（1- = []⇒升= [] ）∧（L = []⇒升=（TL升）[ HD L ]）
⇒∀我：项目・（∃ X 1，X 2 ：列表・ X = X 1 [我] X 2 ⇔∃ ÿ 1，Y 2 ：列表・ X = ÿ 1 [我] ý 2）） ）
然后可以用证明器SETHEO证明。
在未来几年，语义网可能代表PL1的重要应用。万维网的内容应该不仅可以解释为人，也可以解释为机器。为此，网站正在以正式描述语言提供其语义描述。因此，在网络中搜索信息将变得比今天更有效，其中基本上只有文本构建块是可搜索的。
可判定的谓词逻辑子集用作描述语言。有效的推理结构的开发非常重要，并且与描述语言密切相关。对未来语义操作搜索引擎的查询可以（非正式地）读到：下周日瑞士在海拔2000米以下的地方是否会有良好的天气和最佳的滑雪场？为了解决这样一个问题，需要一个能够快速处理大量事实和规则的微积分。在这里，复杂的嵌套函数术语不太重要。
作为基本描述框架，万维网联盟开发了语言RDF（资源描述框架）。在RDF的基础上，显着更强大的语言OWL（Web Ontology Language）允许描述对象和对象类之间的关系，类似于PL1 [SET09]。本体是对可能对象之间关系的描述。
