論文の概要: Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology

• arxiv url: http://arxiv.org/abs/2610.08214v1
• Date: Tue, 06 Oct 2026 12:07:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-08 02:58:29.970225
• Title: Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
• Title（参考訳）: 論理学を教える数学的補足:LogiKEy法
• Abstract要約: 本稿では,計算機科学・数学・哲学生の混成グループに論理を教えるためのアプローチについて報告する。 コース,サマースクール,チュートリアルで10年以上使用されている論理的多元論的なLogiKEy手法を用いている。
• 参考スコア（独自算出の注目度）: 0.22940141855172033
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We report on an approach to teaching logic to mixed groups of computer science, mathematics, and philosophy students, based on the logico-pluralistic LogiKEy methodology, used for more than a decade in courses, summer schools, and tutorials. LogiKEy uses classical higher-order logic (HOL) as a universal metalogic in which object logics, classical and non-classical alike, are encoded by defining their semantics; through these semantical embeddings a single proof assistant (e.g. Isabelle/HOL), with its automated theorem provers and (counter-)model finders, becomes one environment in which students learn, experiment with, and compare logics. After making the pedagogical case for proof assistants in the logic classroom, we present a graded sequence of classroom examples, each transition motivated by a limitation of the preceding representation, by a need for more explicit modelling resources, or by a new application. A liars-and-truth-tellers puzzle leads from propositional to modal logic; the Wise Men puzzle leads on to dynamic epistemic logic; Boolos's curious inference illustrates what a higher-order meta-logic buys, even for automated proof search; Chisholm's paradox takes the sequence into deontic logic, and from standard to dyadic deontic logic; and Gödel's ontological argument brings it to a research-level metaphysical argument. We then rebut the objection that embedding everything in classical HOL is monism rather than pluralism, reflect on three years of teaching such a course, and sketch the portability of the approach beyond Isabelle.
• Abstract（参考訳）: 本稿では,コンピュータ科学・数学・哲学生の混成グループに論理学を教えるためのアプローチについて,論理学・多元論のLogiKEy方法論を10年以上コース,サマースクール,チュートリアルで用いたアプローチについて報告する。 LogiKEy は古典的高階論理 (HOL) を、古典的および非古典的論理のように、それらの意味論を定義することによって符号化される普遍的メタロジック(英語版)として使用し、これらの意味論的埋め込みにより、その自動定理プロバーと(対数)モデルファインダを備えた単一の証明アシスタント (eg Isabelle/HOL) が、学生が論理を学び、実験し、比較する1つの環境となる。 論理教室における証明アシスタントの教育的ケースを作成した後、より明示的なモデリングリソースの必要性、あるいは新しいアプリケーションによって、前述した表現の制限によって動機づけられた各遷移の段階的な事例を示す。 リアーズ・アンド・トゥルース・テラーズパズルは命題論理からモーダル論理へと導かれる; ワイズ・メンのパズルはダイナミック・エピステミック論理に導かれる; ブーロスの好奇心は、自動証明探索でも高次のメタ論理的購入がどのようなものかを示す; チゾムのパラドックスは、列をデオン論理に、そして標準からディヤド・デオン論理に導かれる; ゲーデルの存在論的議論は、研究レベルのメタ論理的議論をもたらす。 次に、古典的HOLにすべてを埋め込むことは、多元主義ではなく単元主義であり、そのようなコースを3年間教えてきたことを反映し、イザベルを超えるアプローチの可搬性について考察する。

関連論文リスト

• Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint) [0.07646713951724012]
  本稿では,LogiKEyのような統一メタロジカルフレームワークにおいて,オブジェクト論理レベルでの論理的多元論を推し進める。 現代の証明助手における論理的多元主義の原則的支持を提唱し、論理的帝国主義に対して警告する。
  論文  参考訳（メタデータ） (2026-05-26T16:25:52Z)
• Faithful Logic Embeddings in HOL -- Deep and Shallow [0.0]
  本稿では,古典的高次論理学における深層・浅層埋め込みの同時展開法を提案する。 この手法は論理学の教育、研究、応用に有用であり、ここでは単純な命題のモーダル論理を用いて説明される。
  論文  参考訳（メタデータ） (2025-02-26T17:08:07Z)
• Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework [117.6508659085231]
  本稿では論理完全推論フレームワークであるAristotleについて,論理解法,論理解法,論理解法,論理解法の3つの主要なコンポーネントを提案する。 本フレームワークでは,記号表現と論理規則を総合的に推論プロセスに統合する。 いくつかのデータセットの実験結果は、Aristotleが最先端の推論フレームワークを精度と効率の両方で一貫して上回っていることを示している。
  論文  参考訳（メタデータ） (2024-12-22T10:14:09Z)
• Empower Nested Boolean Logic via Self-Supervised Curriculum Learning [67.46052028752327]
  大規模言語モデルを含む事前学習された言語モデルは、多言語論理に直面するランダムセレクタのように振る舞う。 この基本的能力で言語モデルを強化するために,本稿では,新たな自己教師付き学習手法であるtextitCurriculum Logical Reasoning (textscClr) を提案する。
  論文  参考訳（メタデータ） (2023-10-09T06:54:02Z)
• LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and Reasoning [73.98142349171552]
  LOGICSEGは、神経誘導学習と論理推論をリッチデータとシンボリック知識の両方に統合する、全体論的視覚意味論である。 ファジィ論理に基づく連続的な緩和の間、論理式はデータとニューラルな計算グラフに基礎を置いており、論理によるネットワークトレーニングを可能にする。 これらの設計によりLOGICSEGは、既存のセグメンテーションモデルに容易に統合できる汎用的でコンパクトなニューラル論理マシンとなる。
  論文  参考訳（メタデータ） (2023-09-24T05:43:19Z)
• Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis [0.0]
  本稿では,議論的言説の深い多元論的論理解析へのアプローチを提案する。 我々は古典的な高階論理に最先端の自動推論技術を用いる。
  論文  参考訳（メタデータ） (2020-07-02T11:07:53Z)
• A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of G\"odel's Ontological Argument [0.0]
  いくつかの議論前提は修正され、他のものは取り下げられ、モダル崩壊は回避され、既に弱いモダル論理 K と T で妥当性が示される。 本稿は, 量子化された非古典論理に対する現代的な知識表現と推論技術が, 新たな知識を他の分野にもたらす方法を説明する。
  論文  参考訳（メタデータ） (2020-01-14T10:26:51Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。