臺大課程網
預選課表

計算邏輯簡介

115-1 開課

  • 流水號

    27720

  • 課號

    CSIE4111

  • 課程識別碼

    902 48130

  • 無分班

  • 3 學分

  • 選修

    資訊工程學系

      選修

    • 資訊工程學系

  • 王柏堯
    • 搜尋教師開設的課程

    • 電機資訊學院 資訊工程學系

    • bywang@iis.sinica.edu.tw

    • 中央研究院資訊科學所新館717室

    • 02-27883799-1717

  • 三 2, 3, 4

  • 資111

  • 2 類

  • 修課總人數 50 人

    本校 40 人 + 外校 10 人

  • 無領域專長

  • 中文授課
  • NTU COOL
  • 核心能力與課程規劃關聯圖
  • 備註
  • 修課限制

    • 限學士班三年級 或 限學士班四年級

  • 本校選課狀況

    已選上
    0/40
    外系已選上
    0/0
    剩餘名額
    0
    已登記
    0
  • 課程概述
    This course gives a general introduction to mathematical logic and its applications in computer science. Mathematical logic is an important foundation of various fields in theoretical computer science. It also has many important applications from program verification to machine-checkable proofs. Through various tools, this course gives a gentle introduction of logic in computer science. It also covers preliminaries for theoretical topics in advanced courses.
  • 課程目標
    To introduce students skills of logical reasoning. To introduce students elements of mathematical logic. To introduce students applications of mathematical logic in computer science.
  • 課程要求
  • 預期每週課前或/與課後學習時數
  • Office Hour
  • 指定閱讀
  • 參考書目
    1. Logic in Computer Science: Modelling and Reasoning about Systems, M. Huth and M. Ryan, Cambridge University Press, 2004. 2. Handbook of Theoretical Computer Science (volume B). The MIT Press, 1994. 3. The SAT Live! homepage. http://www.satlive.org 4. The SMT-LIB homepage. http://www.smtlib.org 5. The ROCQ homepage. https://rocq-prover.org 6. The SPIN homepage. https://spinroot.com
  • 評量方式
    50%

    Homework

    20%

    Midterm

    20%

    Final

    10%

    Attendence

    1. 本校建議 A+ 比例上限為 20% ，非強制規定， 授課教師可依課程要求調整，建議必修課程參考。
    2. 本校採用等第制評定成績，學生成績評量辦法中的百分制分數區間與單科成績對照表僅供參考，授課教師可依等第定義調整分數區間。詳見 學習評量專區。
  • 針對學生困難提供學生調整方式
  • 補課資訊
  • 課程進度
    09/09第 1 週Propositional Logic - Natural Deduction
    09/16第 2 週Propositional Logic - Natural Deduction, Semantics
    09/23第 3 週Propositional Logic - Semantics, Soundness and Completeness
    09/30第 4 週Propositional Logic - Normal Forms, SAT Solver
    10/07第 5 週Predicate Logic - Natural Deduction
    10/14第 6 週Predicate Logic - Semantics, Undecidability
    10/21第 7 週Predicate Logic - Expressiveness, Rocq Proof Assistant
    10/28第 8 週midterm
    11/04第 9 週Program Verification - Hoare Logic
    11/11第 10 週Program Verification - Hoare Logic, Z3 SMT Solver
    11/18第 11 週Model Checking - Linear-Time Temporal Logic
    11/25第 12 週Model Checking - Linear-Time Temporal Logic, SPIN Model Checker
    12/02第 13 週Model Checking - Branch-Time Temporal Logic, CTL*, Model Checking Algorithms
    12/09第 14 週Model Checking - Model Checking Algorithms
    12/16第 15 週Model Checking - Model Checking Algorithms, Fixed-Point Characterization of CTL
    12/23第 16 週Final exam
  • 為確保您我的權利，請尊重智慧財產權及不得非法影印。