数理論理学

TypeScript

TypeScript でシーケント計算自動化（トークン化編）

命題論理のシーケント自動計算機 - Tokenizer の実装 やりたいこと シーケント計算自動化 形式手法を使えるようになりたいと思って何度か Alloy に取り組んでみましたが，根本的に数理論理学がわかっていないので，一旦数理論理学を勉...
2020.08.11
TypeScript数理論理学
数理論理学

モデル検査入門の PDF を読んだまとめ 3（完結）

モデル検査入門の PDF を読んだまとめ 2の続きです． 第 6 章　CTL モデル検査 モデル検査を実施するためには， 検証したいシステムを Kripke モデル M として表現し， 検証したい性質を状態論理式 \varphi で表し（...
2020.05.05
数理論理学
数理論理学

モデル検査入門の PDF を読んだまとめ 2

モデル検査入門の PDF を読んだまとめ 1のつづき． 第 3 章　様相理論 K 様相理論は「今後どうなる」みたいな時相を取り扱うことになる． そのために，K-論理式を定義して（論理演算子 \Box を追加する）おく． 状態遷移を取り扱うた...
2020.05.05
数理論理学
数理論理学

モデル検査入門の PDF を読んだまとめ1

「モデル検査入門」でググると上位に京大の数理研 2009 年の講義ノートと思われる PDF が見つかるので読んでみた．自分用のまとめなので他人の参考にならないかもしれない．詳しくは PDF 探して読んでください． モデル検査入門 ここでは「...
2020.05.05
数理論理学