論文の概要: The Coq Proof Script Visualiser (coq-psv)
- arxiv url: http://arxiv.org/abs/2101.07761v1
- Date: Fri, 15 Jan 2021 08:52:31 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-15 02:55:57.746343
- Title: The Coq Proof Script Visualiser (coq-psv)
- Title(参考訳): coq 証明スクリプト visualiser (coq-psv)
- Authors: Mario Frank
- Abstract要約: このツールは、すべての証明ステップを視覚化できるので、教育とレビューのプロセスの両方をサポートする。
証明をハイパーテキストやマークダウン文書として視覚化する一般的な手法とは対照的に、生成されたファイルを簡単に印刷することができる。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: In this work, we present a visualisation tool that is able to process Coq
proof scripts and generate a table representation of the contained proofs as
$\LaTeX$ or PDF files. This tool has the aim to support both education and
review processes as all proof steps can be visualised. Thus, there is no need
to use Coq in order to review proofs or use them as examples in teaching. In
contrast to the usual approach of visualising proofs as hypertext or markdown
documents, the generated files can be easily printed.
- Abstract(参考訳): 本稿では,coq証明スクリプトを処理し,格納された証明のテーブル表現を$\latex$またはpdfファイルとして生成する可視化ツールを提案する。
このツールは、すべての証明ステップを可視化できるため、教育とレビュープロセスの両方をサポートすることを目的としている。
したがって、証明をレビューしたり、教えの例として使うためにCoqを使う必要はない。
証明をハイパーテキストやマークダウンドキュメントとして視覚化するという一般的なアプローチとは対照的に、生成されたファイルを簡単に印刷できる。
関連論文リスト
- Towards Automatic Transformations of Coq Proof Scripts [0.0]
後続スクリプト変換を行うためのフレームワークを提案する。
これらの変換は、証明が完了すると、自動化された後処理ステップとして適用される。
当社のツールは,GeoCoqライブラリなど,さまざまなCoq証明スクリプトに適用しています。
論文 参考訳(メタデータ) (2024-01-22T12:48:34Z) - In-Context Pretraining: Language Modeling Beyond Document Boundaries [141.22670357089385]
In-Context Pretrainingは、言語モデルが関連するドキュメントのシーケンスで事前トレーニングされる新しいアプローチである。
本稿では, 近接探索を効率的に行うための近似アルゴリズムを提案する。
より複雑なコンテキスト推論を必要とするタスクの顕著な改善が見られます。
論文 参考訳(メタデータ) (2023-10-16T17:57:12Z) - Advancing Visual Grounding with Scene Knowledge: Benchmark and Method [74.72663425217522]
ビジュアルグラウンドディング(VG)は、視覚と言語の間にきめ細かいアライメントを確立することを目的としている。
既存のVGデータセットの多くは、単純な記述テキストを使って構築されている。
我々は、アンダーラインScene underline-guided underlineVisual underlineGroundingの新たなベンチマークを提案する。
論文 参考訳(メタデータ) (2023-07-21T13:06:02Z) - Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
仮説文書埋め込み(英: hypothetical Document Embeddings, HyDE)は、ゼロショット高密度検索システムである。
我々は,HyDEが最先端の非教師付き高密度検索器であるContrieverを著しく上回っていることを示す。
論文 参考訳(メタデータ) (2022-12-20T18:09:52Z) - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。
大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文 参考訳(メタデータ) (2022-10-21T22:37:22Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳(メタデータ) (2022-05-25T02:22:30Z) - Unified Pretraining Framework for Document Understanding [52.224359498792836]
文書理解のための統合事前学習フレームワークであるUDocを紹介する。
UDocは、ほとんどのドキュメント理解タスクをサポートするように設計されており、Transformerを拡張してマルチモーダル埋め込みを入力とする。
UDocの重要な特徴は、3つの自己管理的損失を利用して汎用的な表現を学ぶことである。
論文 参考訳(メタデータ) (2022-04-22T21:47:04Z) - Proof Blocks: Autogradable Scaffolding Activities for Learning to Write
Proofs [0.4588028371034407]
Proof Blocksは、学生が事前に書かれた証明行を正しい順序にドラッグ&ドロップすることで、証明を書くことができるソフトウェアツールである。
これらの証明は完全に自動的に評価され、学生は自分の証明で何をしているのかを素早くフィードバックすることができる。
問題を構築する際、インストラクターは証明の行の依存性グラフを指定し、行の正しい配置をフルクレジットで受け取れるようにする。
論文 参考訳(メタデータ) (2021-06-07T17:03:58Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳(メタデータ) (2020-12-20T18:15:12Z) - Evidence-Aware Inferential Text Generation with Vector Quantised
Variational AutoEncoder [104.25716317141321]
本稿では,大規模なテキストコーパスからイベントの証拠を自動的に発見し,その証拠を利用して推論テキストの生成を導く手法を提案する。
このアプローチは、Event2MindとATOMICの両方のデータセットで最先端のパフォーマンスを提供します。
論文 参考訳(メタデータ) (2020-06-15T02:59:52Z) - Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。
システムの性能は、Coq Standard Libraryで評価される。
CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
論文 参考訳(メタデータ) (2020-03-20T08:22:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。