論文の概要: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for Program Verification via Operational Semantics

• arxiv url: http://arxiv.org/abs/2404.18098v1
• Date: Sun, 28 Apr 2024 07:08:44 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-30 17:53:05.964031
• Title: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for Program Verification via Operational Semantics
• Title（参考訳）: パラメータ化動的論理 - 操作意味論によるプログラム検証のための循環論理フレームワークを目指して
• Authors: Yuanrui Zhang,
• Abstract要約: 本稿では,DLpと呼ばれるパラメータ化動的論理型論理式を提案する。 プログラムの動作意味に基づくシンボリックな実行に基づいている。 ケーススタディは、DLpが異なるタイプのプログラムを推論するためにどのように機能するかを示すために分析される。
• 参考スコア（独自算出の注目度）: 0.174048653626208
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Dynamic logic and its variations, because of their good expressive forms capturing program specifications clearly by isolating programs from logical formulas, have been used as a formalism in program reasoning for decades and have many applications in different areas. The program models of traditional dynamic logics are in explicit forms. With a clearly-defined syntactic structure, compositional verification is made possible, in which a deduction step transfers proving a program into proving its sub-programs. This structure-based reasoning forms the basis of many dynamic logics and popular Hoare-style logics. However, structural rules induce a major drawback that for different target programs, different rules have to be proposed to adapt different program structures. Moreover, there exist programs that does not support (or not entirely support) a structure-based reasoning. In this paper, we propose a parameterized `dynamic-logic-like' logic called DLp with general forms of program models and formulas, and propose a cyclic proof system for this logic. Program reasoning in DLp is directly based on symbolic executions of programs according to their operational semantics. This reduces the burden of designing a large set of rules when specializing a logic theory to a specific domain, and facilitates verifying programs without a suitable structure for direct reasoning. Without reasoning by dissolving program structures, DLp can cause an infinite proof structure. To solve this, we build a cyclic preproof structure for the proof system of DLp and prove its soundness. Case studies are analyzed to show how DLp works for reasoning about different types of programs.
• Abstract（参考訳）: 動的論理とその変種は、プログラムを論理式から分離することでプログラム仕様をはっきりと捉える優れた表現形式のため、何十年もプログラム推論における形式主義として使われてきた。 伝統的な動的論理のプログラムモデルは明示的な形式である。 明確に定義された構文構造により、推論ステップがプログラムの証明をサブプログラムの証明に転送する構成検証が可能である。 この構造に基づく推論は多くの動的論理と人気のあるホアスタイル論理の基礎を形成する。 しかし、構造規則は、異なるターゲットプログラムに対して、異なるプログラム構造に対応するために異なるルールを提案する必要があるという大きな欠点を生じさせる。 さらに、構造に基づく推論をサポートしていない(あるいは完全にサポートしていない)プログラムも存在する。 本稿では,プログラムモデルと公式の一般的な形式を用いたDLpと呼ばれるパラメータ化された動的論理型論理を提案し,この論理の循環的証明システムを提案する。 DLpのプログラム推論は、プログラムの動作意味性に応じてプログラムのシンボル的実行を直接ベースとする。 これにより、論理理論を特定の領域に専門化する際に、大きなルールセットを設計する負担を軽減し、直接推論に適した構造を持たないプログラムの検証を容易にする。 プログラム構造を解かなければ、DLpは無限の証明構造を引き起こす。 これを解決するために, DLp の証明システムのための周期的事前防御構造を構築し, その健全性を証明する。 ケーススタディは、DLpが異なるタイプのプログラムを推論するためにどのように機能するかを示すために分析される。

関連論文リスト

• The Stable Model Semantics for Higher-Order Logic Programming [4.106754434769354]
  本稿では,高階論理プログラムのための安定モデルセマンティクスを提案する。 我々のセマンティクスは、強力な形式主義である近似固定点理論(AFT)を用いて開発されている。 安定モデルセマンティクスの下での高階論理プログラミングは強力で汎用的な形式であることを示す。
  論文  参考訳（メタデータ） (2024-08-20T06:03:52Z)
• A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
  本稿では,マルチエージェント,知識ベース,動的システムのモデリングと解析のための統合フレームワークを提案する。 モデリング側では,このようなフレームワークを実用的な目的に使いやすくするプロセス代数的,エージェント指向の仕様言語を提案する。
  論文  参考訳（メタデータ） (2024-07-24T08:35:50Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。 応用例としては、メタ理論的性質の形式的解析と検証がある。
  論文  参考訳（メタデータ） (2023-12-08T09:32:26Z)
• LOGICSEG: Parsing Visual Semantics with Neural Logic Learning and Reasoning [73.98142349171552]
  LOGICSEGは、神経誘導学習と論理推論をリッチデータとシンボリック知識の両方に統合する、全体論的視覚意味論である。 ファジィ論理に基づく連続的な緩和の間、論理式はデータとニューラルな計算グラフに基礎を置いており、論理によるネットワークトレーニングを可能にする。 これらの設計によりLOGICSEGは、既存のセグメンテーションモデルに容易に統合できる汎用的でコンパクトなニューラル論理マシンとなる。
  論文  参考訳（メタデータ） (2023-09-24T05:43:19Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。 線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
  論文  参考訳（メタデータ） (2023-05-23T01:25:29Z)
• Language Model Cascades [72.18809575261498]
  テスト時に1つのモデルで繰り返し対話する、あるいは複数のモデルの合成は、さらに機能を拡張する。 制御フローと動的構造を持つ場合、確率的プログラミングのテクニックが必要となる。 この観点から、スクラッチパッド/思考連鎖、検証器、STaR、選択推論、ツール利用など、いくつかの既存のテクニックを定式化します。
  論文  参考訳（メタデータ） (2022-07-21T07:35:18Z)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。 対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
  論文  参考訳（メタデータ） (2021-10-18T10:45:59Z)
• Reactive Answer Set Programming [2.7286395031146062]
  Logic Production System (LPS)は、リアクティブな振る舞いをモデル化するためのロジックベースのフレームワークである。 本稿では,このフレームワーク(KELPS)のカーネルを解集合プログラム(ASP)に体系的にマッピングする。
  論文  参考訳（メタデータ） (2021-09-22T10:10:14Z)
• A Logical Characterization of the Preferred Models of Logic Programs with Ordered Disjunction [1.7403133838762446]
  順序付き解法(LPOD)を用いた論理プログラムのための新しいモデル論的意味論を提供する。 提案手法は従来のLPODのセマンティクスの欠点を克服するものである。 新しいアプローチは、節の先頭に順序と古典的な分岐の両方を持つことができる論理プログラムの自然なクラスの意味を定義するために使われる。
  論文  参考訳（メタデータ） (2021-08-07T05:36:12Z)
• On Quantified Modal Theorem Proving for Modeling Ethics [0.0]
  量子化されたモーダル論理は、二重効果、ウクライナ、美徳倫理の教義の様々なバージョンをモデル化するために使われてきた。 我々はこれらの特徴を概説し、DCECのいくつかの側面の証明自動化に役立つアルゴリズムのスケッチを示す。
  論文  参考訳（メタデータ） (2019-12-30T15:14:21Z)

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

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