論文の概要: On systematic construction of correct logic programs

• arxiv url: http://arxiv.org/abs/2508.16782v1
• Date: Fri, 22 Aug 2025 20:27:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-26 18:43:45.175197
• Title: On systematic construction of correct logic programs
• Title（参考訳）: 正しい論理プログラムの体系的構築について
• Authors: Włodzimierz Drabent,
• Abstract要約: 本稿では,証明可能な論理プログラムと半完全論理プログラムを体系的に構築する手法を提案する。 提案手法は単純で,実際の日常プログラミングで(非公式に)使用することができる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces all the answers required by the specifications. We also consider semi-completeness -- completeness for those queries for which the program does not diverge. This paper presents an approach to systematically construct provably correct and semi-complete logic programs, for a given specification. Normal programs are considered, under Kunen's 3-valued completion semantics (of negation as finite failure) and the well-founded semantics (of negation as possibly infinite failure). The approach is declarative, it abstracts from details of operational semantics, like e.g.\ the form of the selected literals (``procedure calls'') during the computation. The proposed method is simple, and can be used (maybe informally) in actual everyday programming.
• Abstract（参考訳）: 命令型あるいは関数型プログラミングの部分的正当性は、論理プログラミングを2つの概念に分ける。 正確性は、プログラムのすべての答えが仕様と互換性があることを意味する。 完全性とは、プログラムが仕様で要求されるすべての答えを生成することを意味する。 また、プログラムが分岐しないクエリに対する半完全性も検討する。 本稿では,特定の仕様に対して,証明可能な論理プログラムと半完全論理プログラムを体系的に構築する手法を提案する。 通常のプログラムは、クネンの3つの評価された完結意味論(有限失敗として否定する)と、十分に確立された意味論(無限失敗の可能性として否定する)に基づいて検討される。 このアプローチは宣言的であり、計算中に選択されたリテラル(``procedure call'')の形式であるe g \のようなオペレーションセマンティクスの詳細を抽象化する。 提案手法は単純で,実際の日常プログラミングで(非公式に)使用することができる。

関連論文リスト

• A Reduction of Input/Output Logics to SAT [51.82266520875928]
  デオン論理(Deontic logic)は、規範、義務、許可、禁止について推論するための形式主義である。 本稿では,I/O論理の自動化手法を提案する。
  論文  参考訳（メタデータ） (2025-08-22T09:22:26Z)
• Relating Answer Set Programming and Many-sorted Logics for Formal Verification [1.223779595809275]
  私の研究課題は、ASP検証をアクセス可能で日常的なタスクにする意図で、3つの問題に対処することに集中しています。 ASP の代替セマンティクスを,この辺りで多種多様な一階述語論理の論理への変換に基づいて検討した。 これらのセマンティクスは、論理プログラムのモジュラー理解を促進し、基底をバイパスし、自動定理プロバーを使用してプログラムのプロパティを自動検証することを可能にする。
  論文  参考訳（メタデータ） (2025-02-13T11:52:40Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• On Feasibility of Declarative Diagnosis [0.0]
  論理プログラムの宣言的診断には有用な方法があり、実際のプログラミングでは有効であるべきだと論じる。 本稿では、その主な弱点について論じ、克服方法を示す。
  論文  参考訳（メタデータ） (2023-08-30T08:56:19Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)
• 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)
• Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
  我々は、本質的にすべての実数値論理をカバーするためにパラメータ化できる、音と強完全公理化を与える。 文のクラスは非常に豊かであり、各クラスは実数値論理の式の集合に対して可能な実値の集合を記述する。
  論文  参考訳（メタデータ） (2020-08-06T02:13:11Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。