論文の概要: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- arxiv url: http://arxiv.org/abs/2404.18098v4
- Date: Wed, 29 Jan 2025 18:43:16 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-01-30 22:32:42.307704
- Title: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- Title（参考訳）: パラメータ化動的論理 - 汎用プログラム仕様と検証のための循環論理フレームワークを目指して
- Authors: Yuanrui Zhang,
- Abstract要約: 本稿では,プログラムモデルの豊富な集合を特定・推論するためのパラメータ化動的論理理論,すなわちDLpについて述べる。
動的論理理論に基づいた柔軟な検証フレームワークを提供する。
- 参考スコア（独自算出の注目度）: 0.174048653626208
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present a theory of parameterized dynamic logic, namely DLp, for specifying and reasoning about a rich set of program models based on their transitional behaviours. Different from most dynamic logics that deal with regular expressions or a particular type of formalisms, DLp introduces a type of labels called "program configurations" as explicit program status for symbolic executions, allowing programs and formulas to be of arbitrary forms according to interested domains. This characteristic empowers dynamic logical formulas with a direct support of symbolic-execution-based reasoning, while still maintaining reasoning based on syntactic structures in traditional dynamic logics through a rule-lifting process. We propose a proof system and build a cyclic preproof structure special for DLp, which guarantees the soundness of infinite proof trees induced by symbolically executing programs with explicit/implicit loop structures. The soundness of DLp is formally analyzed and proved. DLp provides a flexible verification framework based on the theories of dynamic logics. It helps reduce the burden of developing different dynamic-logic theories for different programs, and save the additional transformations in the derivations of non-compositional programs. We give some examples of instantiations of DLp in particular domains, showing the potential and advantages of using DLp in practical usage.
- Abstract（参考訳）: 本稿では、パラメータ化動的論理理論、すなわちDLpについて、その遷移挙動に基づいてプログラムモデルのリッチなセットを特定し、推論する。
正規表現や特定の形式を扱うほとんどの動的論理とは異なり、DLpは「プログラム構成」と呼ばれるラベルのタイプを記号的実行の明示的なプログラムステータスとして導入し、プログラムと公式は興味のあるドメインに従って任意の形式にすることができる。
この特性は、シンボリック・エグゼクティオンに基づく推論を直接サポートしながら、ルールリフトプロセスを通じて従来の動的論理の構文構造に基づく推論を維持しながら、動的論理式を補強する。
本稿では,明示的かつ単純なループ構造を持つプログラムを象徴的に実行することによって生じる無限の証明木の健全性を保証し,DLpに特有な周期的事前防御構造を構築することを提案する。
DLpの音質を解析し, 検証した。
DLpは動的論理理論に基づいた柔軟な検証フレームワークを提供する。
これは、異なるプログラムに対して異なる動的論理学理論を開発することの負担を軽減するのに役立ち、非構成的プログラムの導出における追加的な変換を省くのに役立つ。
本稿では, DLp のインスタンス化を事例として, DLp の実用的利用の可能性と利点を示す。
関連論文リスト
- On the Logical Content of Logic Programs [0.0]
本稿では,プログラムが知っていることを説明するサポートの関係を定義することで,論理プログラミング(LP)の新たな視点を紹介する。
結果は、証明理論のセマンティクスにおける基本拡張セマンティクスの考え方を用いて定式化される。
提案手法は,LPの論理的基礎に関する新たな知見を提供し,知識表現や自動推論,形式的検証などに応用できる可能性がある。
論文 参考訳（メタデータ） (2025-03-07T11:58:08Z) - Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups [0.0]
本稿では、算術やブール演算以外の同型暗号を直観論理の領域に拡張するための概念的枠組みを提案する。
ソフトウェア最適化やハードウェアアクセラレーションなど,このアプローチを潜在的に効率的にするための戦略を概説する。
論文 参考訳（メタデータ） (2025-02-26T10:10:10Z) - 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) - 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) - Language Model Cascades [72.18809575261498]
テスト時に1つのモデルで繰り返し対話する、あるいは複数のモデルの合成は、さらに機能を拡張する。
制御フローと動的構造を持つ場合、確率的プログラミングのテクニックが必要となる。
この観点から、スクラッチパッド/思考連鎖、検証器、STaR、選択推論、ツール利用など、いくつかの既存のテクニックを定式化します。
論文 参考訳（メタデータ） (2022-07-21T07:35:18Z) - 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) - 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) - Implementing Dynamic Answer Set Programming [0.0]
動的論理式を時間論理プログラムに変換する。
動的論理式を時間論理プログラムに還元することで、両方のアプローチでASPを一様に拡張できます。
論文 参考訳（メタデータ） (2020-02-17T12:34:14Z) - On Quantified Modal Theorem Proving for Modeling Ethics [0.0]
量子化されたモーダル論理は、二重効果、ウクライナ、美徳倫理の教義の様々なバージョンをモデル化するために使われてきた。
我々はこれらの特徴を概説し、DCECのいくつかの側面の証明自動化に役立つアルゴリズムのスケッチを示す。
論文 参考訳（メタデータ） (2019-12-30T15:14:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。