論文の概要: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- arxiv url: http://arxiv.org/abs/2404.18098v3
- Date: Wed, 7 Aug 2024 12:41:15 GMT
- ステータス: 処理完了
- システム内更新日: 2024-08-08 15:25:48.710311
- Title: Parameterized Dynamic Logic -- Towards A Cyclic Logical Framework for General Program Specification and Verification
- Title（参考訳）: パラメータ化動的論理 - 汎用プログラム仕様と検証のための循環論理フレームワークを目指して
- Authors: Yuanrui Zhang,
- Abstract要約: 本稿では,パラメータ化された動的論理型形式である$DL_p$を提案する。
$DL_p$は、異なる動的論理理論を包含する柔軟な検証フレームワークを提供する。
ケーススタディは、$DL_p$が異なるタイプのプログラムモデルについて推論するためにどのように機能するかを示している。
- 参考スコア（独自算出の注目度）: 0.174048653626208
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Dynamic logic and its variations, because of their clear and expressive forms for capturing program properties, have been used as formalisms in program/system specification and verification for years and have many other applications. The program models of dynamic logics are in explicit forms. For different target program models, different dynamic logic theories have to be proposed to adapt different models' semantics. In this paper, we propose a parameterized `dynamic-logic-style' formalism, namely $DL_p$, for specifying and reasoning about general program models. In $DL_p$, program models and logical formulas are taken as `parameters', allowing arbitrary forms according to different interested domains. This characteristic allows $DL_p$ to support direct reasoning based on the operational semantics of program models, while still preserving compositional reasoning based on syntactic structures. $DL_p$ provides a flexible verification framework to encompass different dynamic logic theories. In addition, it also facilitates reasoning about program models whose semantics is not compositional, examples are neural networks, automata-based models, synchronous programming languages, etc. We mainly focus on building the theory of $DL_p$, including defining its syntax and semantics, building a proof system and constructing a cyclic preproof structure. We analyze and prove the soundness of $DL_p$. Case studies show how $DL_p$ works for reasoning about different types of program models.
- Abstract（参考訳）: 動的論理とそのバリエーションは、プログラム特性を捉えるための明確で表現力のある形式のため、プログラム/システム仕様と検証の形式として長年使われてきた。
動的論理のプログラムモデルは明示的な形式である。
異なる対象のプログラムモデルに対して、異なるモデルのセマンティクスを適用するために異なる動的論理理論が提案される必要がある。
本稿では,汎用プログラムモデルの定義と推論のためのパラメータ化'動的論理型'形式,すなわち$DL_p$を提案する。
DL_p$ では、プログラムモデルと論理式は「パラメータ」として扱われ、異なる関心領域に応じて任意の形式が許される。
この特性により、$DL_p$は、構文構造に基づく構成的推論を保持しながら、プログラムモデルの操作的セマンティクスに基づいて直接推論をサポートすることができる。
$DL_p$は、異なる動的論理理論を包含する柔軟な検証フレームワークを提供する。
さらに、セマンティクスが構成的でないプログラムモデル、例えばニューラルネットワーク、オートマタベースのモデル、同期プログラミング言語などについても推論を容易にする。
主に$DL_p$の理論の構築に焦点をあて、構文と意味論を定義し、証明システムを構築し、循環型防食構造を構築する。
我々は$DL_p$の音質を分析し、証明する。
ケーススタディは、$DL_p$が異なるタイプのプログラムモデルについて推論するためにどのように機能するかを示している。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。