图 书 馆
自动推理的概述Overview of Automated Reasoning |
|
| 课程网址: | http://videolectures.net/ssll09_norrish_oar/ |
| 主讲教师: | Michael Norrish |
| 开课单位: | 澳大利亚信息通信技术研究中心 |
| 开课时间: | 2009-04-01 |
| 课程语种: | 英语 |
| 中文简介: |  |
| 课程简介: | 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. |
| 关 键 词: | 计算机逻辑推理; 对偶问题; 交互式定理 |
| 课程来源: | 视频讲座网 |
| 最后编审: | 2020-06-06：zyk |
| 阅读次数: | 83 |