图 书 馆
图表推理可以自动化吗Can diagrammatic reasoning be automated |
|
| 课程网址: | http://videolectures.net/solomon_jamnik_cdra/ |
| 主讲教师: | Mateja Jamnik |
| 开课单位: | 剑桥大学 |
| 开课时间: | 2007-02-25 |
| 课程语种: | 英语 |
| 中文简介: |  |
| 课程简介: | Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the "inference steps" of the proof. \\ An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive omega-rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the meta-theory of diagrams. These ideas have been implemented in the system, called DIAMOND, which is presented here. |
| 关 键 词: | 自动定理; 形式逻辑; 普遍量化定理 |
| 课程来源: | 视频讲座网 |
| 最后编审: | 2019-09-22：cwx |
| 阅读次数: | 51 |