0


自动推理综述

Overview of Automated Reasoning
课程网址: http://videolectures.net/ssll09_baumgartner_oar/  
主讲教师: Peter Baumgartner
开课单位: 澳大利亚国立大学
开课时间: 2009-04-01
课程语种: 英语
中文简介:
课程说明:在许多应用程序中,我们希望计算机进行逻辑推理。我们可能天真地希望这是计算机擅长的领域,但是实际上他们发现这非常困难。在本概述课程中,我们简要介绍几种机械推理。第一种是自动演绎,其结论是完全根据假设通过假设得出的,而无需用户干预。自动演绎程序通过其推理的逻辑进行参数化。我们区分命题逻辑和一阶逻辑。命题逻辑程序(也称为SAT解算器)的开发和应用在过去十年中受到了相当大的关注,例如在解决约束满足问题,在硬件设计,验证以及计划和调度中的应用。关于一阶逻辑的自动演绎,我们讨论应用程序,标准演绎过程(例如解析度)和基本概念(例如统一)。我们还研究了定理证明的对偶问题,即生成给定理论的模型,该模型可用于寻找非定理的反例。本课程涵盖的第三个重要领域是交互式定理证明。交互式定理证明需要用户提供一定数量的指令,以告诉证明程序(定理证明者)如何进行证明。通常需要这种交互,这是因为使用了更高阶的逻辑,这些逻辑的表达形式主义允许对复杂系统(例如操作系统或各种协议)进行自然建模。交互式证明开发的最新趋势是通过结合自动证明的功能来提高其自动化程度。
课程简介: Course Description:In many applications, we expect computers to reason logically. We might naively expect this to be what computers are good at, but in fact they find it extremely difficult. In this overview course, we look briefly at several varieties of mechanical reasoning. The first is automated deduction, whereby conclusions are derived from assumptions purely by following an algorithm, without user intervention. Automated deduction procedures are parametrized by the logic they are capable of reasoning with. We distinguish between propositional logic and first-order logic. Development and application of propositional logic procedures, also called SAT solvers, received considerable attention in the last ten years, e.g., for solving constraint satisfaction problems, applications in hardware design, verification, and planning and scheduling. Regarding automated deduction in first-order logic, we discuss applications, standard deductive procedures such as resolution, and basic concepts, such as unification. We also examine the dual problem of theorem proving, viz., generating models of a given theory, which has applications to finding counterexamples for non-theorems. A third important area covered in the course is dealing with interactive theorem proving. Interactive theorem proving requires certain amount of instructions from the user to tell the proving program (the theorem prover) how to proceed with a proof. Such interaction is required usually because of the use of higher-order logics, whose expressive formalisms allow natural modeling of complex systems, such as operating system or various protocols. A recent trend in the development of interactive proving is to improve its automation, by combining the power of automatic provers.
关 键 词: 逻辑推理; 自动演绎; 解算器
课程来源: 视频讲座网
最后编审: 2019-09-23:cwx
阅读次数: 58