Fugu-MT 論文翻訳(概要): Verifying Tight Logic Programs with anthem and Vampire

論文の概要: Verifying Tight Logic Programs with anthem and Vampire

arxiv url: http://arxiv.org/abs/2008.02025v6
Date: Mon, 1 May 2023 17:19:20 GMT
ステータス: 処理完了
システム内更新日: 2023-05-02 22:38:10.053050
Title: Verifying Tight Logic Programs with anthem and Vampire
Title（参考訳）: アンセムとヴァンパイアによるタイト論理プログラムの検証
Authors: Jorge Fandinno, Vladimir Lifschitz, Patrick L\"uhne and Torsten Schaub
Abstract要約: プログラム完了の定義を、ASPのグルーダーグリンゴの入力言語のサブセットで入力と出力を持つプログラムに拡張する。本稿では,この文脈における安定モデルと完成度の関係について検討し,2つのソフトウェアツールを用いた予備実験について述べる。
参考スコア（独自算出の注目度）: 7.804960968120875
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Under consideration for acceptance in TPLP.
Abstract（参考訳）: 本稿では,論理プログラムと一階理論の関係を調べることを目的とした研究を継続する。我々は,プログラム完了の定義を,ASPの接頭辞の入力言語のサブセットで入力と出力を持つプログラムに拡張し,安定モデルと完了との関係について検討し,入力と出力によるプログラムの正当性を検証するために,アンセムとヴァンパイアという2つのソフトウェアツールを用いた予備実験を記述する。定理の証明は、この論文で研究されたプログラムのセマンティクスを一階式の安定モデルに関連付ける補題に基づいている。 TPLPの受容についての検討

関連論文リスト

Sequential decomposition of propositional logic programs [0.0]
本稿では,プログラム間のグリーンの関係を研究することによって,プログラムの逐次分解について検討する。より広い意味では、この論文は論理プログラミングの代数的理論へのさらなる一歩である。
論文参考訳（メタデータ） (2023-02-21T16:14:57Z)
Hybrid Probabilistic Logic Programming: Inference and Learning [1.14219428942199]
この論文は確率論的論理プログラミング(PLP)の進歩に焦点を当てており、不確実性の確率理論と関係性のための論理プログラミングを組み合わせたものである。最初のコントリビューションは、コンテクスト固有の非依存性を計算ゲインに活用する新しいサンプリングアルゴリズムであるCS-LWの導入である。次に、新しいハイブリッドPLPであるDC#が導入され、分散クロースとベイズ論理プログラムの構文を統合し、3種類の独立性を表す。スケーラブルな推論アルゴリズムFO-CS-LWがDC#で導入された。
論文参考訳（メタデータ） (2023-02-01T15:07:36Z)
Hierarchical Programmatic Reinforcement Learning via Learning to Compose Programs [58.94569213396991]
プログラムポリシーを作成するための階層型プログラム強化学習フレームワークを提案する。提案するフレームワークは,プログラム作成の学習を通じて,アウト・オブ・ディストリビュータの複雑な動作を記述するプログラムポリシーを作成することができる。 Karel ドメインの実験結果から,提案するフレームワークがベースラインより優れていることが示された。
論文参考訳（メタデータ） (2023-01-30T14:50:46Z)
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)
Verification of Locally Tight Programs [8.005641341294732]
プログラム完了は、論理プログラムの言語から一階理論の言語への変換である。この定理の厳密性条件は、より制限の少ない「局所的厳密性」要件に置き換えることができることを示す。証明アシスタントAnthem-p2pは、局所的に密なプログラム間の等価性を検証できると結論付ける。
論文参考訳（メタデータ） (2022-04-18T23:22:54Z)
Planning with Incomplete Information in Quantified Answer Set Programming [1.3501640559999886]
ASP(Answer Set Programming)における不完全な情報を用いた計画手法を提案する。論理プログラムが状態間の遷移関数を記述する単純な形式主義を用いて計画問題を表現している。本稿では、量子化された論理プログラムをQBFに変換し、QBFソルバを実行する翻訳ベースのQASPソルバを提案する。
論文参考訳（メタデータ） (2021-08-13T21:24:47Z)
Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
論文参考訳（メタデータ） (2021-07-13T03:48:04Z)
Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
入力出力の例からCプログラムを合成する第一歩を踏み出す。特に,部分生成プログラムの実行を近似するために潜在表現を学習するLa Synthを提案する。これらのプログラムのトレーニングにより,Karel と C のプログラム合成における予測性能がさらに向上することを示す。
論文参考訳（メタデータ） (2021-06-29T02:21:32Z)
Latent Programmer: Discrete Latent Codes for Program Synthesis [56.37993487589351]
プログラム合成や文書要約などの多くのシーケンス学習タスクにおいて、重要な問題は出力シーケンスの広い空間を探索することである。本稿では,検索対象とする出力の表現を学習することを提案する。本稿では,まず入力/出力サンプルから離散潜在コードを予測するプログラム合成手法であるemphLatent Programmerを紹介し,そのプログラムを対象言語で生成する。
論文参考訳（メタデータ） (2020-12-01T10:11:35Z)

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