Fugu-MT 論文翻訳(概要): Teaching Higher-Order Logic Using Isabelle

論文の概要: Teaching Higher-Order Logic Using Isabelle

arxiv url: http://arxiv.org/abs/2404.05458v1
Date: Mon, 8 Apr 2024 12:40:27 GMT
ステータス: 処理完了
システム内更新日: 2024-04-09 14:34:53.520847
Title: Teaching Higher-Order Logic Using Isabelle
Title（参考訳）: Isabelle を用いた高次論理教育
Authors: Simon Tobias Lund, Jørgen Villadsen,
Abstract要約: 我々はイザベル証明アシスタントにおいて高階論理の形式化を示す。これは、高階論理と証明アシスタントについて学ぼうとする人にとっては、良い紹介になるはずだ。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.
Abstract（参考訳）: 本稿では,Isabelle/Pure を基盤として,Isabelle/Pure をベースとした高階論理の定式化を行い,可能な限り小型かつ可読性を実現した。したがって、より複雑なIsabelle/HOLを重く自動化することなく、高階論理と証明アシスタントについて学ぼうとする人にとって、これは良い紹介となるはずです。本研究の展開とアプローチを紹介するため,本論文では,高階論理の公理と規則を解説し,授業環境における教科教育の経験について論じる。

関連論文リスト

Exploring the Role of Reasoning Structures for Constructing Proofs in Multi-Step Natural Language Reasoning with Large Language Models [30.09120709652445]
本稿では,現在最先端のジェネラリスト LLM がいくつかの例でこれらの構造を活用でき,テキスト・コンテクスト・ラーニングによる証明構造をより良く構築できるかどうかという,焦点を絞った研究に焦点をあてる。
論文参考訳（メタデータ） (2024-10-11T00:45:50Z)
Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
大規模言語モデル(LLM)に基づくKG上の複雑な推論スキーマを提案する。任意の一階論理クエリを二分木分解により拡張し、LLMの推論能力を刺激する。広く使われているデータセットに対する実験では、LACTは高度な手法よりも大幅に改善されている(平均+5.5% MRRスコア)。
論文参考訳（メタデータ） (2024-05-02T18:12:08Z)
LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models [52.03659714625452]
最近開発された大規模言語モデル (LLM) は、幅広い言語理解タスクにおいて非常によく機能することが示されている。しかし、それらは自然言語に対して本当に「理性」があるのだろうか? この疑問は研究の注目を集めており、コモンセンス、数値、定性的など多くの推論技術が研究されている。
論文参考訳（メタデータ） (2024-04-23T21:08:49Z)
Logic-Scaffolding: Personalized Aspect-Instructed Recommendation Explanation Generation using LLMs [20.446594942586604]
我々は、アスペクトベースの説明とチェーン・オブ・思想のアイデアを組み合わせて、中間的推論ステップを通じて説明を生成するLogic-Scaffoldingというフレームワークを提案する。本稿では,フレームワーク構築の経験を共有し,その結果を探索するためのインタラクティブなデモンストレーションを行う。
論文参考訳（メタデータ） (2023-12-22T00:30:10Z)
An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。応用例としては、メタ理論的性質の形式的解析と検証がある。
論文参考訳（メタデータ） (2023-12-08T09:32:26Z)
Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文参考訳（メタデータ） (2023-05-23T01:25:29Z)
On Exams with the Isabelle Proof Assistant [0.0]
本稿では,Isabelle証明アシスタントを用いた自動推論のコースにおいて,学生の学習結果をテストするためのアプローチを提案する。このアプローチにより、様々な論理的証明システムにおける形式的証明の一般的な理解と、イザベル/HOLの高階論理における証明の理解の両方をテストすることができる。
論文参考訳（メタデータ） (2023-03-10T11:37:09Z)
elBERto: Self-supervised Commonsense Learning for Question Answering [131.51059870970616]
本稿では、市販QAモデルアーキテクチャと互換性のあるコモンセンスフレームワークの自己教師型双方向表現学習を提案する。このフレームワークは5つの自己教師型タスクから構成されており、リッチコモンセンスを含むコンテキストから追加のトレーニング信号を完全に活用するようモデルに強制する。 elBERtoは、単純な語彙的類似性比較が役に立たないような、アウト・オブ・パラグラフや非エフェクトな問題に対して、大幅に改善されている。
論文参考訳（メタデータ） (2022-03-17T16:23:45Z)
New Algebraic Normative Theories for Ethical and Legal Reasoning in the LogiKEy Framework [0.0]
古典的な高階論理へのデオン論理のセマンティック埋め込みに基づくLogiKEy手法を提案する。代数的アプローチを用いて,LogiKEyデオン論理とデータセットを大幅に拡張する。
論文参考訳（メタデータ） (2021-07-25T16:33:07Z)
Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
論理的な記号や表現をテキストで理解し、答えにたどり着くよう提案します。このような論理的情報に基づいて,文脈拡張フレームワークとデータ拡張アルゴリズムを提案する。本手法は最先端の性能を実現し,論理駆動コンテキスト拡張フレームワークとデータ拡張アルゴリズムの両方が精度向上に寄与する。
論文参考訳（メタデータ） (2021-05-08T10:09:36Z)

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