形式／非形式とレイヤー構成 - 檜山正幸のキマイラ飼育記 メモ編にシーケントが出てこないが、シーケントは構文形式なので、幾つかの使い途がある。 基本推論図は、ひとつのシーケントで表現可能で、基本推論図とそのシーケントは同一視してもよい。 一般の…

大分類 非形式 形式化データ 備考 計算 対象式 対象式（項） もともと形式化されている 論理 命題 論理式 文字列または構文解析木 論理 推論 推論図 仮定と結論がある 論理 リーズニング リーズニング図 ツリー状ノード・ワイヤー図 すべての形式化データは…

「一貫性」という言葉が曖昧だから整理する。まず、律子〈rator〉は法則を与える2-射（あるいはもっと高次の射）のこと。律子が満たす等式を制約等式〈constraint equation〉または等式的制約〈equational constraint〉または単に制約〈constraint〉と呼ぶ。…