論文の概要: 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が異なるタイプのプログラムを推論するためにどのように機能するかを示すために分析される。
関連論文リスト
- 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) - Modeling Hierarchical Reasoning Chains by Linking Discourse Units and
Key Phrases for Reading Comprehension [80.99865844249106]
本稿では,論理的推論の基盤として,対話レベルと単語レベルの両方の文脈を扱う総合グラフネットワーク(HGN)を提案する。
具体的には、ノードレベルの関係とタイプレベルの関係は、推論過程におけるブリッジと解釈できるが、階層的な相互作用機構によってモデル化される。
論文 参考訳（メタデータ） (2023-06-21T07:34:27Z) - Argumentative Characterizations of (Extended) Disjunctive Logic Programs [2.055949720959582]
仮定に基づく議論は、通常の論理プログラムだけでなく、解法論理プログラムとその拡張も表現できることを示す。
議論フレームワークの中核となるロジックが尊重すべき解離の推論ルールについて考察する。
論文 参考訳（メタデータ） (2023-06-12T14:01:38Z) - Query Structure Modeling for Inductive Logical Reasoning Over Knowledge
Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。
線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。
2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文 参考訳（メタデータ） (2023-05-23T01:25:29Z) - Logic of Differentiable Logics: Towards a Uniform Semantics of DL [1.1549572298362787]
論理的仕様を満たすためにニューラルネットワークを訓練する方法として、微分論理(DL)が提案されている。
本稿では、微分可能論理学(LDL)と呼ばれるDLを定義するメタ言語を提案する。
我々は,既存のDLの理論的特性を確立するためにLDLを使用し,ニューラルネットワークの検証において実験的な研究を行う。
論文 参考訳（メタデータ） (2023-03-19T13:03:51Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文)
論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。
ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
論文 参考訳（メタデータ） (2022-07-04T14:38:49Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。
対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
論文 参考訳（メタデータ） (2021-10-18T10:45:59Z) - Implementing Dynamic Answer Set Programming [0.0]
動的論理式を時間論理プログラムに変換する。
動的論理式を時間論理プログラムに還元することで、両方のアプローチでASPを一様に拡張できます。
論文 参考訳（メタデータ） (2020-02-17T12:34:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。