論理と形式化

  [ GB12601 ]
Introduction to First-order Logic and Formalization
対象:2学年 開設学期:春AB 曜日・時限:金3・4 単位数:2単位
担当教員:水谷哲也, 海野広志

概要

ソフトウェア科学や人工知能など,種々の分野で用いられる論理式の正確な読み書きと証明の方法,論理学の情報科学への応用等を理解する.

学習・教育目標

命題論理および一階述語論理の形式体系と意味論を理解し,論理による形式化の手法を習得する.また,論理を使ったプログラミングなど,情報科学への論理の応用について学ぶ.

キーワード

一階述語論理,自然演繹法,形式体系,証明,導出原理.

Keywords

first-order logic, natural deduction, formal system, proof, resolution.

時間割

講義内容/理解すべき項目
第1週(担当: 水谷) 論理とは何か:実例・応用・様々な論理,論理式による表現,情報科学における論理.
第2週(担当: 水谷) 一階述語論理の意味及び体系: 意味論,形式体系,一階言語,自然演繹 (NK).
第3-6週(担当: 水谷) 一階述語論理の証明:様々な論理式の証明,演習.
第7-9週(担当: 海野) 命題論理・一階述語論理の計算:証明探索、導出原理、単一化、SAT、SMT.
第10週(担当: 海野) 発展的な内容、授業のまとめ.

教材

講義で配布,もしくは,ウェブページを通じて配布する.

参考書籍

前原昭二: 記号論理入門[新装版],日本評論社,2005.
小野寛晰: 情報科学における論理,日本評論社,1994.
鹿島亮: 数理論理学,朝倉書店,2009.

予備知識・前提条件

「離散構造」の内容を修得していることが望ましい.

成績評価

授業への出席を前提として,期末試験(50%),レポート及び演習成績(50%)により評価する.

教員メールアドレス

水谷:mizutani (at) cs (dot) tsukuba (dot) ac (dot) jp
海野:uhiro (at) cs (dot) tsukuba (dot) ac (dot) jp

講義のWebページ

海野担当分 http://logic.cs.tsukuba.ac.jp/~uhiro/logic/

オフィスアワー

水谷: 木5限 3F708 
海野: 金5限 SB907