1 論理式の概要
1.1 論理式の定義と役割
1.1.1 構文による表現
論理式は、記号の組合せとして定義される。変数、定数（真偽に対応する語や記号）、論理演算子（否定、論理積、論理和、含意など）を用い、規則に従って有限の長さで構成される。構文の目的は、記号列が「論理式として正しく書けているか」を機械的に判定できる形にすることにある。 このとき重要なのは、見た目の並びが恣意的であってはならず、演算子の結合の仕方や括弧の扱いが明確に規定される点である。構文だけでは真偽は決まらないが、意味論への橋渡しとなる。
1.1.2 意味論による真偽の決定
意味論は、論理式に対して「ある解釈のもとで真か偽か」を与える。典型的には、変数に対して真理値（真または偽）を割り当て、その割当と演算子の意味規則に従って、式全体の値を計算する。 この枠組みにより、同じ構文でも解釈が異なれば評価結果も変わりうること、逆に構文が同一なら意味論計算の手続きが一意に定まることが保証される。
1.2 命題と変数
1.2.1 命題変数
命題変数は、真偽が未確定な「成分」を表すための記号である。たとえば「P」「Q」のように書かれ、意味論では各変数に真理値を割り当てることで、式の評価が可能になる。 変数を導入する利点は、個別の具体的主張に依存せず、主張同士の関係や推論の一般パターンを抽出できる点にある。
1.2.2 定数（真・偽）の扱い
真・偽の定数は、評価の際に変数の代わりに固定値を与えるための要素である。これにより、常に成立する主張や常に成立しない主張を論理式の中で直接表現できる。 定数を含む場合でも意味論の手続きは一貫しており、演算子の規則に従って真理値が計算される。
2 論理演算と構文
2.1 否定（否定演算）
否定は、ある式の真偽を反転させる演算子として扱われる。式 A が偽なら否定は真になり、A が真なら否定は偽になる。構文上は、対象となる式の前に記号を置く形や、記号と括弧で包む形で表されることが多い。 否定は単独でも、他の演算子と組み合わせても重要で、後続の変形規則（たとえば双対性）にも深く関わる。
2.2 論理積・論理和
2.2.1 連言（かつ）
連言は、両方の構成要素がともに成立するときのみ真となる演算である。直観的には「両方とも成り立つ」ことを表す。 評価では、それぞれの部分式の真偽を調べ、双方が真であるときだけ真理値を真にする。
2.2.2 隔言（または）
隔言は、少なくとも一方が成立するときに真となる演算として定義される。つまり「どちらか一方でも成り立つ」場合に真となる。 この演算も評価は部分式の真偽に依存し、真が存在すれば真が返る。
2.3 条件と関係
2.3.1 ならば（含意）
含意は、前件が真で後件が偽であるときだけ偽になり、それ以外では真とされる。直観的には「前件が成り立つなら後件も成り立つはずだ」という関係を表すが、真理値表の定義に従うのが要点である。 この定義は、形式的推論や自動判定の体系と整合するように設計されている。
2.3.2 同値（恒真・等価の表現）
同値は、両側の真偽が一致するときに真になる演算である。つまり一方が真なら他方も真、片方が偽なら他方も偽という関係を表す。 さらに、同値の考え方は「式がいつでも同じ値をとる」こと、すなわち等価性の概念とも結びつく。これにより、複数の表現が同一の意味を持つかを扱えるようになる。
2.4 括弧と優先順位
2.4.1 見通しのための括弧
括弧は、演算子の結合の順序を明示し、式の解釈を確定するために用いられる。構文上、括弧により部分式の境界がはっきりするため、意味論計算でもどこから評価するかが明確になる。 特に複雑な式では、括弧を適切に入れることで読みやすさと解釈の一意性が向上する。
2.4.2 優先順位の規則
優先順位は、括弧がない場合にどの演算子から結合を解釈するかを規定する。たとえば、ある体系では否定が最も強く結合し、論理積が論理和より強い、といった規約が与えられる。 優先順位があることで、同じ構文でも書き方の簡略化が可能になるが、規約の理解を誤ると別の式として扱われる危険があるため、体系ごとのルールを参照する必要がある。
3 論理式の評価と推論
3.1 解釈と充足
3.1.1 充足可能性
充足可能性は、「ある真偽割当が存在して、論理式が真になるか」を問う性質である。真になる割当が一つでも見つかれば充足可能であり、どの割当でも偽なら充足不可能である。 この判定は、組合せ探索の形で捉えられる場合があり、計算資源の見積もりやアルゴリズム設計の出発点になる。
3.1.2 真偽割当（評価）
真偽割当は、各命題変数に対して真理値を対応づけることである。評価は、その割当と演算子の定義に従って、式の値を段階的に決めていく操作として定義される。 評価は論理式の木構造（部分式の階層）に沿って計算できるため、形式検証や自動推論において繰り返し利用される基礎手続きになる。
3.2 妥当性と論理的含意
3.2.1 妥当（恒真）とは
妥当性は、論理式がどの割当のもとでも真であることに対応する。恒真とも呼ばれ、評価の観点では「反例が存在しない」ことを意味する。 この性質が重要なのは、推論の正当性が妥当な前提から妥当な結論へ伝播する設計と関係するためである。
3.2.2 含意関係の判定
論理的含意は、ある式 B が別の式 A の論理的帰結として成り立つかを扱う。形式的には「A を真にする割当が存在するとき、必ず B も真になる」こととして規定される。 判定には、含意の否定が充足可能かどうかへ帰着させるなど、実装上の工夫が用いられることが多い。
3.3 等価変形と簡約
3.3.1 ド・モルガン則
ド・モルガン則は、否定と論理積・論理和の関係を示す変形規則である。連言の否定が隔言の否定へ、隔言の否定が連言の否定へ対応する形で表される。 これにより、否定を内側へ押し込む、あるいは外側へ整理するような書き換えが可能になり、正規形構築の基礎になる。
3.3.2 双対性と置換
双対性は、論理演算子の入れ替え規則により、ある式の性質を対応する形へ移す考え方である。たとえば「積と和」「真と偽」「否定の向き」などを一貫した対応で入れ替えると、同型の関係が得られる。 置換は、同値である部分式を別の同値表現へ置き換える操作であり、式を簡潔にする目的で使われる。
3.3.3 正規形への変換
正規形は、論理式をある標準的な形に変形することで比較・判定を扱いやすくする枠組みである。変換によって同値性が保たれるように設計され、以後の処理（充足性判定、含意判定、簡約）で計算量や実装効率に影響する。 変換には一般に、否定の位置整理や分配則の適用が含まれ、結果として式の大きさが増える場合もある。
4 論理式の代表的な形式
4.1 帰結計算（証明の枠組み）
4.1.1 推論規則の考え方
帰結計算では、式の集合から別の式を導くための推論規則を用いる。各規則は、前提となる式（または式の列）が満たされるなら結論が成立する、という関係を形式的に規定する。 この枠組みの利点は、真偽値を直接列挙するのではなく、導出の手続きとして証明を表現できる点にある。
4.1.2 証明可能性の概念
証明可能性は、「ある式が規則体系のもとで導出できるか」を問う性質である。導出できるなら、その体系では結論が前提から正当に得られると解釈される。 また、証明可能性と意味論上の妥当性が一致するかどうかは、体系の性質として研究対象になる。
4.2 通常形（正規形）
4.2.1 判定用の形への変換
通常形（ここでは正規形の一種として扱う）は、充足性や含意の判定を実行しやすい形へ論理式を写す方法である。変形の狙いは、判定手続きが部分構造に依存しやすくなるよう、表現の制約を加えることにある。 変換により同値が保証される場合と、充足可能性の保全のみが保証される場合があるため、使用目的に応じた選択が必要となる。
4.2.2 CNFとDNFの位置づけ
CNF（積標準形）とDNF（和標準形）は、論理式をそれぞれ「論理積の形」や「論理和の形」の階層に整理する代表的な枠組みである。各構成要素はさらに簡約された単位（節や項）ででき、充足性判定やアルゴリズムへの入力として扱われる。 一般に、ある問題はCNF側が扱いやすく、別の問題はDNF側が有利になることがあり、変換コストと併せて検討される。
4.3 応用分野での扱い
4.3.1 形式検証
形式検証では、ハードウェアやソフトウェアの仕様を論理式で表し、実装が仕様を満たすかを自動的に確かめる。典型的には、違反が起きる状態を示す式が充足可能かどうか、あるいは妥当性が成り立つかを判定する。 ここでは論理式が、曖昧な記述を検証可能な形へ落とし込む共通の媒体になる。
4.3.2 充足性問題とソルバ
充足性問題は、与えられた論理式が充足可能かを調べる問題である。ソルバは、この判定を機械的に行うための推論・探索手続きの総称であり、大規模な式に対しても実用的な性能を目指して改良されてきた。 現場では、入力形式の整形（正規形への変換など）や前処理によって探索を効率化し、解を見つける、または不可能性を示す、という形で結果を返す。