論文の概要: Formal Semantics and Formally Verified Validation for Temporal Planning
- arxiv url: http://arxiv.org/abs/2203.13604v1
- Date: Fri, 25 Mar 2022 12:04:03 GMT
- ステータス: 処理完了
- システム内更新日: 2022-03-28 18:49:22.250466
- Title: Formal Semantics and Formally Verified Validation for Temporal Planning
- Title(参考訳): 形式的意味論と時間計画のための形式的検証
- Authors: Mohammad Abdulaziz, Lukas Koller
- Abstract要約: 時間計画のための簡潔で簡潔な意味論を提示する。
このセマンティクスは対話型定理証明器 Isabelle/HOL の論理で開発・形式化されている。
我々はこれらのセマンティクスから時間計画のための検証アルゴリズムを導き、Isabelle/HOLの形式的証明を用いて、この検証アルゴリズムが我々のセマンティクスを実装していることを示す。
- 参考スコア(独自算出の注目度): 7.538482310185133
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present a simple and concise semantics for temporal planning. Our
semantics are developed and formalised in the logic of the interactive theorem
prover Isabelle/HOL. We derive from those semantics a validation algorithm for
temporal planning and show, using a formal proof in Isabelle/HOL, that this
validation algorithm implements our semantics. We experimentally evaluate our
verified validation algorithm and show that it is practical.
- Abstract(参考訳): 時間計画のための簡潔で簡潔な意味論を提示する。
このセマンティクスは対話型定理証明器 Isabelle/HOL の論理で開発・形式化されている。
これらのセマンティクスから時間計画のための検証アルゴリズムを導出し、イザベル/ホルの形式的証明を用いて、この検証アルゴリズムが我々のセマンティクスを実装していることを示す。
検証アルゴリズムを実験的に評価し,実用的であることを示す。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - Learning Temporal Logic Predicates from Data with Statistical Guarantees [0.0]
有限サンプル精度保証データから時間論理の述語を学習する新しい手法を提案する。
提案手法は,表現最適化と共形予測を利用して,将来の軌跡を正しく記述した述語を学習する。
論文 参考訳(メタデータ) (2024-06-15T00:07:36Z) - Formally Verified Approximate Policy Iteration [11.602089225841633]
形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。
実装は、その実行可能性を示すために、ベンチマーク問題で評価される。
この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
論文 参考訳(メタデータ) (2024-06-11T15:07:08Z) - A Fixed-Point Approach to Unified Prompt-Based Counting [51.20608895374113]
本研究の目的は,ボックス,ポイント,テキストなど,さまざまなプロンプト型で示されるオブジェクトの密度マップを生成することができる包括的プロンプトベースのカウントフレームワークを確立することである。
本モデルは,クラスに依存しない顕著なデータセットに優れ,データセット間の適応タスクにおいて優れた性能を示す。
論文 参考訳(メタデータ) (2024-03-15T12:05:44Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳(メタデータ) (2023-01-05T17:56:00Z) - Logical Satisfiability of Counterfactuals for Faithful Explanations in
NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。
これは、説明に表される論理述語に基づいて、反実仮説を生成する。
そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文 参考訳(メタデータ) (2022-05-25T03:40:59Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。
最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
論文 参考訳(メタデータ) (2020-10-23T19:08:46Z) - Counterfactual Detection meets Transfer Learning [48.82717416666232]
既存のモデルアーキテクチャに最小限の適応で実装可能な,単純なバイナリ分類タスクであることを示す。
本稿では,先行者や後続者をエンティティ認識タスクとして処理するエンド・ツー・エンドパイプラインを導入し,それらをトークン分類に適用する。
論文 参考訳(メタデータ) (2020-05-27T02:02:57Z) - Adaptive Teaching of Temporal Logic Formulas to Learners with
Preferences [44.63937003271641]
時間論理式に対する機械教育について検討する。
ミオピック溶液の徹底的な探索には指数的時間を要する。
パラメトリック線形時間論理式を効率よく教える手法を提案する。
論文 参考訳(メタデータ) (2020-01-27T18:22:53Z) - Understanding the QuickXPlain Algorithm: Simple Explanation and Formal
Proof [0.0]
本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。
他のアルゴリズムを証明するためのガイダンスとして使用できる。
また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
論文 参考訳(メタデータ) (2020-01-07T01:37:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。