桜技録

🐈🐈🐈🐈🐘

数学

ノート: 情報科学における論理④

小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。(→前回) 第2章 述語論理(承前) 古典述語論理の形式体系LK 推論規則 古典命題論理での推論規則に加えて次の推論規則を持つ。なお は論理式、 は論理式の列、 は任意の項、 は…

ノート: 情報科学における論理③

間が空いてしまったけれど小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。(→前回) 2021-11-13 読み返してて気になる点があったので一部を訂正 第2章 述語論理 述語論理の論理式 言語 述語論理を記述するのに必要な以下の記号…

ノート: 情報科学における論理②

小野寛晰『情報科学における論理』の読書ノート。(→前回) 第1章 命題論理(承前) 今回はシークエント計算を実装してみる。 定理1.8の証明で登場した式の分解を推論規則に、完全分解木を証明図に流用したいので、形式体系LKそのままではなくそれを少し変形…

ノート: 情報科学における論理①

小野寛晰『情報科学における論理』の読書ノート。なるべく練習問題も解いてく。 2021-11-07 読み返してて気になる点があったので一部を訂正 第1章 命題論理 古典命題論理の形式体系LK 式 式(sequent)は次の形式によって表現される。 ここで は論理式を表す…