論文の概要: Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
- arxiv url: http://arxiv.org/abs/2505.05988v1
- Date: Fri, 09 May 2025 12:18:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-12 20:40:10.256956
- Title: Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned
- Title(参考訳): 一階論理を教えるための最小連続計算:学習した教訓
- Authors: Jørgen Villadsen,
- Abstract要約: MiniCalcは、最小シーケンスの計算に基づいて一階述語論理を教えるWebアプリである。
オプションとして、証明はイザベル証明アシスタントで検証できる。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: MiniCalc is a web app for teaching first-order logic based on a minimal sequent calculus. As an option the proofs can be verified in the Isabelle proof assistant. We present the lessons learned using the tool in recent years at our university.
- Abstract(参考訳): MiniCalcは、最小シーケンスの計算に基づいて一階述語論理を教えるWebアプリである。
オプションとして、証明はイザベル証明アシスタントで検証できる。
近年,このツールを用いて学んだ教訓を大学に紹介する。
関連論文リスト
- LogicLearner: A Tool for the Guided Practice of Propositional Logic Proofs [2.649019945607464]
我々は、ガイド付き論理証明実践のためのWebアプリケーションであるLogicLearnerを開発した。
LogicLearnerは、ステップバイステップで論理証明を試みるインターフェースと、オンザフライでソリューションを生成する自動証明解決器で構成されている。
論文 参考訳(メタデータ) (2025-03-25T02:23:08Z) - Teaching Higher-Order Logic Using Isabelle [0.0]
我々はイザベル証明アシスタントにおいて高階論理の形式化を示す。
これは、高階論理と証明アシスタントについて学ぼうとする人にとっては、良い紹介になるはずだ。
論文 参考訳(メタデータ) (2024-04-08T12:40:27Z) - InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning [98.53491178426492]
InternLM2から事前学習を継続するILMs InternLM-Mathをオープンソースとして公開する。
我々は、連鎖推論、報酬モデリング、形式推論、データ拡張、コードインタプリタを、統一されたSeq2seqフォーマットで統一する。
我々の事前学習モデルは、微調整なしでMiniF2Fテストセットで30.3を達成する。
論文 参考訳(メタデータ) (2024-02-09T11:22:08Z) - Learning logic programs by finding minimal unsatisfiable subprograms [24.31242130341093]
最小不満足なサブプログラム (MUSP) を識別する ILP アプローチを導入する。
プログラム合成やゲームプレイなど,複数の領域での実験を行った結果,学習時間を99%短縮できることがわかった。
論文 参考訳(メタデータ) (2024-01-29T18:24:16Z) - Optimally Teaching a Linear Behavior Cloning Agent [29.290523215922015]
線形行動クローニング(LBC)学習者の最適指導について検討する。
この設定では、教師はLBC学習者に示す状態を選択することができる。
学習者は、証明と整合した無限線型仮説のバージョン空間を維持する。
論文 参考訳(メタデータ) (2023-11-26T19:47:39Z) - First-Step Advantage: Importance of Starting Right in Multi-Step Math Reasoning [11.75364271481855]
言語モデルは、予測のための合理性を生成することを学ぶことによって、複雑な推論タスクをよりよく解決することができる。
より小さなモデル、特に修正された場合には、彼らが他の方法で苦労したであろうタスクを解決できることを観察します。
我々はQuestCoTを提案し、より小さなモデルがまず、推論の連鎖で進む前に、どのように開始するかを自問する。
論文 参考訳(メタデータ) (2023-11-14T06:45:31Z) - How to escape sharp minima with random perturbations [48.095392390925745]
平らなミニマの概念とそれらを見つける複雑さについて研究する。
一般的なコスト関数に対して、近似平坦な局所最小値を求める勾配に基づくアルゴリズムについて論じる。
コスト関数がトレーニングデータよりも経験的リスクであるような環境では、シャープネス認識最小化と呼ばれる最近提案された実用的なアルゴリズムにインスパイアされたより高速なアルゴリズムを提案する。
論文 参考訳(メタデータ) (2023-05-25T02:12:33Z) - JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem
Understanding [74.12405417718054]
本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。
他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。
基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
論文 参考訳(メタデータ) (2022-06-13T17:03:52Z) - Rethinking Few-Shot Image Classification: a Good Embedding Is All You
Need? [72.00712736992618]
メタトレーニングセット上で教師付きあるいは自己教師型表現を学習する単純なベースラインが、最先端の数ショット学習方法より優れていることを示す。
追加の増量は自己蒸留によって達成できる。
我々は,この発見が,画像分類ベンチマークとメタ学習アルゴリズムの役割を再考する動機となっていると考えている。
論文 参考訳(メタデータ) (2020-03-25T17:58:42Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。