ホーア論理（Hoare Logic、別名 Floyd–Hoare Logic）は、アントニー・ホーアが開発した形式体系。ホーアの1969年の論文 "An axiomatic basis for computer programming" で発表された。この体系の目的は、数理論理学の厳密さでプログラムの正当性を論じるための論理的規則群を提供することにある。

ホーアは、フローチャートに関して同様の体系を発表したロバート・フロイドからの影響を認めている。

ホーア論理の中心となる部分は Hoare Triple である。Hoare Triple はコードの実行による状態変化を表すものである。Hoare Triple の形式は以下の通りである。

<math>\{P\}\;C\;\{Q\}</math>

ここで、P と Q は「表明(assertion)」であり、C は「コマンド」である。P は「事前状態」、Qは「事後状態」でもある。表明（状態）は述語論理の式で表される。

ホーア論理には、単純な命令型言語の全構成要素についての公理と推論規則が備わっている。当初の論文にあったそれら規則に加えて、ホーアや他の研究者は様々な言語要素に関する規則を開発した。並行性に関する規則、プロシージャに関する規則、分岐に関する規則、ポインタに関する規則などがある。