ホーア論理 - Wikipedia

この記事の正確性に疑問が呈されています。問題箇所に信頼できる情報源を示して、記事の改善にご協力ください。議論はノートを参照してください。（2016年4月） 疑問点：トリプルの定義からすでに通常の定義と異なっている。例もおかしい ホーア論理（ホーアろんり、英: Hoare logic）とは、公理的意味論の立場でプログラムの正当性について厳密に推論するために第一階述語論理を拡張した形式論理の言語を言う。 プログラムの正しさを証明するためのロバート・フロイドによる流れ図に関する方法[1]を基に、計算機科学者のアントニー・ホーアによって提案された[2]。 概要[編集] ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に

[hamamuratakuo]

コンピュータサイエンスにおける様相論理｜森北出版株式会社 https://www.morikita.co.jp/books/mid/085641

[masterq]

うん全然知らない。。。 #orz

[h_you]

数理論理学の厳密さでプログラムの正当性を論じるための論理的規則群を提供する