Loading article…
コンピュータ科学における論理学は、論理学とコンピュータ科学の分野が重なり合う領域を網羅しています。この分野は、大きく3つの領域に分けられます。
論理学はコンピュータ科学において基本的な役割を果たしています。論理学の主要分野の中で特に重要なものとしては、計算可能性理論（以前は再帰理論と呼ばれていました）、様相論理、圏論などが挙げられます。計算理論は、アロンゾ・チャーチやアラン・チューリングといった論理学者や数学者によって定義された概念に基づいています。[ 1 ] [ 2 ]チャーチは、ラムダ定義可能性の概念を用いて、アルゴリズム的に解決不可能な問題 の存在を初めて示しました。チューリングは、機械的手順と呼べるものについて初めて説得力のある分析を行い、クルト・ゲーデルはチューリングの分析が「完璧」であると主張しました。[ 3 ]さらに、論理学とコンピュータ科学の理論的な重なり合う主要な分野には、以下のようなものがあります。
人工知能という用語を最初に用いたアプリケーションの一つは、 1956年にアレン・ニューウェル、クリフ・ショー、ハーバート・サイモンによって開発されたロジック・セオリスト・システムでした。論理学者が行うことの一つは、論理の命題の集合を受け取り、論理法則によって真でなければならない結論（追加の命題）を推論することです。例えば、「すべての人間は死ぬ」と「ソクラテスは人間である」という命題が与えられた場合、妥当な結論は「ソクラテスは死ぬ」です。もちろんこれは些細な例です。実際の論理システムでは、命題は多数かつ複雑になる可能性があります。この種の分析はコンピュータの使用によって大幅に助けられることが早くから認識されていました。ロジック・セオリストは、バートランド・ラッセルとアルフレッド・ノース・ホワイトヘッドが数学論理に関する影響力のある著作『プリンキピア・マテマティカ』で行った理論的研究を検証しました。さらに、その後のシステムは、論理学者によって新しい数学の定理や証明を検証および発見するために利用されてきました。[ 7 ]
人工知能（AI）の分野は、常に数理論理学から強い影響を受けてきました。この分野の黎明期から、論理推論を自動化する技術が、問題を解決し、事実から結論を導き出す上で大きな可能性を秘めていることが認識されていました。ロン・ブラフマンは、すべてのAI知識表現形式を評価するための基準として、一階述語論理（FOL）を提唱しました。一階述語論理は、情報を記述・分析するための一般的かつ強力な手法です。FOL自体がコンピュータ言語として使われない理由は、表現力が強すぎるためです。つまり、FOLは、どんなに強力なコンピュータでも解けないようなステートメントを容易に表現できてしまうのです。そのため、あらゆる知識表現形式は、ある意味で表現力と計算可能性のトレードオフと言えます。言語の表現力が強ければ強いほど（つまり、FOLに近ければ近いほど）、処理速度が遅くなり、無限ループに陥りやすくなるという考え方が多く見られます。[ 8 ]しかし、 Heng Zhang らによる最近の研究[ 9 ]では、この考えは厳密に異議を唱えられています。彼らの研究結果は、すべての普遍的な知識表現形式が再帰的に同型であることを示しています。さらに、彼らの証明は、FOL が、計算的に実行可能なオーバーヘッド、具体的には決定論的多項式時間内、あるいはそれよりも低い複雑さで、チューリング マシンによって定義される純粋な手続き的知識表現形式に変換できることを示しています。[ 9 ]
例えば、エキスパートシステムで使用されるIF-THENルールは、一階述語論理のごく限られた部分集合に近似します。論理演算子の全範囲を含む任意の式ではなく、出発点は論理学者がモーダス・ポネンスと呼ぶものです。その結果、ルールベースシステムは、特に最適化アルゴリズムとコンパイルを活用する場合、高性能な計算をサポートできます。[ 10 ]
一方、一階述語論理のホーン節部分集合と非単調な否定形式を組み合わせた論理プログラミングは、高い表現力と効率的な実装の両方を備えています。特に、論理プログラミング言語Prologはチューリング完全なプログラミング言語です。Datalogは関係データベースモデルを再帰的な関係で拡張し、解答集合プログラミングは、困難な（主にNP困難な）探索問題に特化した論理プログラミングの一形態です。
論理理論のもう 1 つの主要な研究分野は、ソフトウェア エンジニアリングです。知識ベース ソフトウェア アシスタントやプログラマー見習いプログラムなどの研究プロジェクトでは、ソフトウェア仕様の正当性を検証するために論理理論が応用されています。また、さまざまなプラットフォームで仕様を効率的なコードに変換し、実装と仕様の等価性を証明するために論理ツールが使用されています。[ 11 ] この形式的な変換主導型アプローチは、従来のソフトウェア開発よりもはるかに手間がかかることがよくあります。しかし、適切な形式と再利用可能なテンプレートを備えた特定のドメインでは、このアプローチは商用製品で実行可能であることが証明されています。適切なドメインは通常、システムの障害が人的または金銭的に非常に大きなコストをもたらす兵器システム、セキュリティ システム、リアルタイム金融システムなどです。そのようなドメインの 1 つは、超大規模集積回路 (VLSI)設計です。これは、CPU やデジタル デバイスのその他の重要なコンポーネントに使用されるチップを設計するプロセスです。チップのエラーは壊滅的な結果を招く可能性があります。ソフトウェアとは異なり、チップはパッチを適用したり更新したりすることはできません。そのため、実装が仕様に対応していることを証明するために形式手法を使用することには商業的な正当性があります。 [ 12 ]
論理学のコンピュータ技術へのもう一つの重要な応用は、フレーム言語と自動分類器の分野です。KL -ONEなどのフレーム言語は、集合論と一階述語論理に直接マッピングできます。これにより、分類器と呼ばれる特殊な定理証明器が、与えられたモデル内の集合、部分集合、関係間のさまざまな宣言を分析できます。このようにして、モデルを検証し、矛盾する定義にフラグを立てることができます。分類器は、新しい情報を推論することもできます。たとえば、既存の情報に基づいて新しい集合を定義したり、新しいデータに基づいて既存の集合の定義を変更したりできます。この柔軟性のレベルは、絶えず変化するインターネットの世界を扱うのに理想的です。分類器技術は、Web Ontology Languageなどの言語の上に構築されており、既存のインターネットの上に論理的な意味レベルを可能にします。このレイヤーはセマンティック Webと呼ばれます。[ 13 ] [ 14 ]
並行システムにおける推論には時間論理が用いられる。[ 15 ]
{{cite book}}ISBN /日付の不一致（ヘルプ）KRシステムが何をするべきかについて非常に明確で具体的な概念が得られたことです。悪い点は、サービスが提供できないことも明らかになったことです...FOLの文が定理であるかどうかを判断することは解決不可能です。