論文の概要: PVS Embeddings of Propositional and Quantified Modal Logic
- arxiv url: http://arxiv.org/abs/2205.06391v1
- Date: Thu, 12 May 2022 22:44:29 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-16 14:09:13.153624
- Title: PVS Embeddings of Propositional and Quantified Modal Logic
- Title(参考訳): 命題論理と量子化モーダル論理のPVS埋め込み
- Authors: John Rushby
- Abstract要約: 本稿では,PVS検証システムにおける命題論理と量子化論理の埋め込みについて述べる。
PVSのリソースは、モーダル論理の標準的な構文の多くをサポートする魅力的な方法でこれを行うことができる。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Modal logics allow reasoning about various modes of truth: for example, what
it means for something to be possibly true, or to know that something is true
as opposed to merely believing it. This report describes embeddings of
propositional and quantified modal logic in the PVS verification system. The
resources of PVS allow this to be done in an attractive way that supports much
of the standard syntax of modal logic, while providing effective automation.
The report introduces and formally specifies and verifies several standard
topics in modal logic such as relationships between the standard modal axioms
and properties of the accessibility relation, and attributes of the Barcan
Formula and its converse in both constant and varying domains.
- Abstract(参考訳): 様相論理は、様々な真理のモードについての推論を可能にする:例えば、何かが真であることの意味や、それを単に信じることとは対照的に、何かが真であることを知る。
本稿では,pvs検証システムにおける命題論理と量化モーダル論理の組込みについて述べる。
PVSのリソースは、効率的な自動化を提供しながら、モーダルロジックの標準的な構文の多くをサポートする魅力的な方法でこれを行うことができる。
本報告では, 標準モーダル公理とアクセシビリティ関係の性質の関係, バーカン公式の属性, および, 定数領域および可変領域におけるその逆関係など, モーダル論理におけるいくつかの標準的トピックを, 正式に定義し, 検証する。
関連論文リスト
- An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳(メタデータ) (2023-12-08T09:32:26Z) - Modeling Hierarchical Reasoning Chains by Linking Discourse Units and
Key Phrases for Reading Comprehension [80.99865844249106]
本稿では,論理的推論の基盤として,対話レベルと単語レベルの両方の文脈を扱う総合グラフネットワーク(HGN)を提案する。
具体的には、ノードレベルの関係とタイプレベルの関係は、推論過程におけるブリッジと解釈できるが、階層的な相互作用機構によってモデル化される。
論文 参考訳(メタデータ) (2023-06-21T07:34:27Z) - An elementary belief function logic [6.091096843566857]
可能性と必要性の尺度、信念と妥当性の関数と不正確な確率の双対性は、モーダル論理と共通の特徴を共有している。
本稿では,MEL上にLukasiewicz論理を追加することにより,より単純な信念関数論理を考案できることを示す。
論文 参考訳(メタデータ) (2023-03-23T10:39:18Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文)
論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。
ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
論文 参考訳(メタデータ) (2022-07-04T14:38:49Z) - Modeling and Automating Public Announcement Logic with Relativized
Common Knowledge as a Fragment of HOL in LogiKEy [0.0]
本稿では,関連する共通知識を用いた発表ロジックのセマンティックな埋め込みについて述べる。
これにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
この研究は、複数派のLogiKEy知識工学方法論に重要な追加となる。
論文 参考訳(メタデータ) (2021-11-02T15:14:52Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。
対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
論文 参考訳(メタデータ) (2021-10-18T10:45:59Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳(メタデータ) (2021-09-25T00:00:47Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳(メタデータ) (2021-07-30T08:27:15Z) - The Possible, the Plausible, and the Desirable: Event-Based Modality
Detection for Language Processing [7.037431698815925]
この研究はGeorgetown Gradable Modal Expressions (GME) のルービンシュタインらによる理論的基礎に基づいている。
本稿では,細粒度モーダル概念の検出と分類を目的としたGMEコーパスの実験を行う。
モーダル表現の検出と分類は可能であるだけでなく,それ自身でモーダル表現を検出できることを示す。
論文 参考訳(メタデータ) (2021-06-15T10:47:57Z) - Public Announcement Logic in HOL [0.0]
関連する共通知識を持つ公開告知論理のための浅層セマンティック埋め込みについて述べる。
この埋め込みにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
論文 参考訳(メタデータ) (2020-10-02T06:46:02Z) - Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
我々は、本質的にすべての実数値論理をカバーするためにパラメータ化できる、音と強完全公理化を与える。
文のクラスは非常に豊かであり、各クラスは実数値論理の式の集合に対して可能な実値の集合を記述する。
論文 参考訳(メタデータ) (2020-08-06T02:13:11Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。