形式科学：逻辑学 - 计算逻辑 - 自动定理证明课程大纲

第1周：课程介绍与预备知识

• 主题：课程概览与逻辑基础
• 学习目标：
  • 理解逻辑学的基本概念：命题、命题逻辑、推理规则
• 阅读/资源：
  • 逻辑导论
  • 在线资源：逻辑基础教程
• 活动：逻辑符号练习
• 评估：入门测验

第2-3周：命题逻辑

• 主题：命题演算和布尔代数
• 学习目标：
  • 掌握命题逻辑的基本结构：合取、析取、否定、蕴含
• 阅读/资源：
  • How to Prove It: A Structured Approach
• 活动：命题逻辑证明实践
• 评估：命题逻辑作业

第4-5周：谓词逻辑

• 主题：一阶谓词逻辑
• 学习目标：
  • 理解量词、函数符号和关系符号的应用
• 阅读/资源：
  • A Concise Introduction to Logic
• 活动：谓词逻辑模型构造
• 评估：谓词逻辑论证项目

第6-7周：自动定理证明概述

• 主题：自动化推理工具（如Prolog, Coq等）
• 学习目标：
  • 了解自动定理证明的基本原理和工作流程
• 阅读/资源：
  • Interactive Theorem Proving
• 活动：使用自动定理证明工具实验
• 评估：自动定理证明小项目

第8-10周：自动定理证明技术深入

• 主题：Herbrand定理、SMT求解器和SAT解法
• 学习目标：
  • 理解自动定理证明的关键算法和技术
• 阅读/资源：
  • Handbook of Practical Logic and Automated Reasoning
• 活动：自动定理证明案例研究
• 评估：自动定理证明研究报告

第11周：课程总结与复习

• 主题：回顾与未来应用
• 学习目标：
  • 总结课程内容并讨论实际应用领域
• 活动：小组讨论与个人展示
• 评估：期末论文或项目

通过本课程，学生将逐步掌握逻辑学的基础知识，并能运用自动定理证明技术解决实际问题。课程设计旨在培养批判性思维和解决问题的能力。