駆け足で読む論理と計算のしくみ

論理と計算のしくみ

論理は考え方とその記載規則
計算機計算は、ヒトが論理を遂行する行為の代行
論理はハードとソフトによって計算機計算用に実装される

• 集合と関係
  • 集合

集合　空集合　部分集合　結びと交わり　直積と直和　関数空間とべき集合　集合族　と
要素　有限集合　外延的　無限集合　内包的　可算　非可算　補集合　互いに素　関数　写像　合成　全射　単射　全単射　部分関数　定義域　全関数　関数空間　特性関数　集合族　添数集合

• • 関係

二項関係　合成と閉包　順序　束　同値関係　クリーネ閉包　反射的　推移的　反対称的　半順序　擬順序　前順序　全順序　上界　下界　上限　下限　

• 命題論理と述語論理

命題　論理記号　構文　意味　ヒルベルト　シーケント計算　導出原理

• • 命題論理

真偽値　連言　宣言　ドモルガン則　含意　同値命題　排他的選言　原子論理式　命題論理式　BNF記法　帰納的定義　省略形　メタ変数　解釈　 if and only if 恒真　トートロジ　排中律　二重否定の除去　決定可能　充足可能　充足不能　無矛盾　演繹体系　公理　定理　推論規則　証明可能　三段論法　健全　完全　リテラル　節　空説　連言標準形　導出　分解　反駁　
コンパクト　

• • 一階述語論理

命題の内部構造も形式化した論理　変数　束縛変数と自由変数　エルブランの定理　述語記号　関数記号　定数　個体変数　領域　一階の変数　二階の変数　項　原子論理式　述語論理式　全称記号　存在記号　量化記号　対象変数　代入　捕獲　付値　汎化　強い完全性　弱い完全性　含意

• • 高階述語論理とその部分体系

二階述語論理　高階述語論理　複数の領域とそれに対応する変数

• 様相論理と直観主義論理

プロセスの経過にしたがって変化するような状況えの論理

• • 命題様相論理

命題最小様相論理　様相記号　必然　可能　可能世界　到達可能性　クリプキ構造　到達可能性関係　必然化　具体化

• • 多重様相論理

ラベル　様相論理間の関係　

• • 時相論理

タブロー法　計算木論理　経路限定子　時相演算子　線形時間時相論理　状態論理式　経路論理式　様相計算　最小不動点　最大不動点　

• • 命題直観主義論理

排中律と二重否定の除去、背理法の成り立たない論理　直観主義論理の真偽値(程度)　命題古典論理は命題直観主義論理の(特殊な)一形態

• 計算可能性
  • チューリング機械

初期状態　状態集合　終了状態　部分関数　チューリング計算可能

• • 帰納的関数

原始機能的　項傾斜関数　射影　原始帰納法　帰納的定義　有界最小化　有限列の符号化　部分帰納的　停止問題　決定不能　帰納的に可算　算術的階層　集合　集合　集合

• • 不完全性定理

完全　不完全　無矛盾　

• • プレスバーガ算出

加算と比較のみの一階の算術　限定子除去

• • 述語論理の決定不能性と決定可能な部分体系
• 計算
  • 項

再帰的関数　再帰的定義　仮引数　実引数　カリー化された関数　複数引数の関数の一引数関数化

• • 簡約

式の一部をより簡単な式で置き換えること　簡約　正規形　チャーチの数字　不動点　不動点演算子　標準化　標準簡約列　最左簡約　簡約戦略　

• • 型付き計算

型付け　正規化可能性　明示的型付け　暗黙的型付け　型判断　型推論　自然演繹　多層型　型抽象